about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/SMTParser.cpp11
-rw-r--r--lib/SMT/SMTParser.h2
-rw-r--r--lib/SMT/main.cpp3
-rw-r--r--lib/SMT/smtlib.y2
4 files changed, 5 insertions, 13 deletions
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 22578f46..03042fdd 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -14,7 +14,6 @@
 #include "klee/Constraints.h"
 #include "expr/Parser.h"
 
-#include <iostream>
 #include <fstream>
 #include <string>
 #include <sstream>
@@ -23,7 +22,6 @@
 
 //#define DEBUG
 
-using namespace std;
 using namespace klee;
 using namespace klee::expr;
 
@@ -103,9 +101,8 @@ bool SMTParser::Solve() {
 
 // XXX: give more info
 int SMTParser::Error(const string& msg) {
-  std::cerr << SMTParser::parserTemp->fileName << ":" 
-	    << SMTParser::parserTemp->lineNum
-	    << ": " << msg << "\n";
+  llvm::errs() << SMTParser::parserTemp->fileName << ":"
+               << SMTParser::parserTemp->lineNum << ": " << msg << "\n";
   exit(1);
   return 0;
 }
@@ -213,7 +210,7 @@ void SMTParser::AddVar(std::string name, ExprHandle val) {
 ExprHandle SMTParser::GetVar(std::string name) {
   VarEnv top = varEnvs.top();
   if (top.find(name) == top.end()) {
-    std::cerr << "Cannot find variable ?" << name << "\n";
+    llvm::errs() << "Cannot find variable ?" << name << "\n";
     exit(1);
   }
   return top[name];
@@ -241,7 +238,7 @@ void SMTParser::AddFVar(std::string name, ExprHandle val) {
 ExprHandle SMTParser::GetFVar(std::string name) {
   FVarEnv top = fvarEnvs.top();
   if (top.find(name) == top.end()) {
-    std::cerr << "Cannot find fvar $" << name << "\n";
+    llvm::errs() << "Cannot find fvar $" << name << "\n";
     exit(1);
   }
   return top[name];
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index fd1ec044..ac84e74c 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -13,8 +13,6 @@
 
 #include "expr/Parser.h"
 
-#include <cassert>
-#include <iostream>
 #include <map>
 #include <stack>
 #include <string>
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 034c4ce4..31fa311d 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -2,9 +2,6 @@
 
 #include "klee/ExprBuilder.h"
 
-#include <iostream>
-
-using namespace std;
 using namespace klee;
 
 int main(int argc, char** argv) {
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 01d3539d..eb3b3890 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -254,7 +254,7 @@ bench_attribute:
   | COLON_TOK LOGIC_TOK logic_name 
     {
       if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") {
-	std::cerr << "ERROR: Logic " << *$3 << " not supported.";
+	llvm::errs() << "ERROR: Logic " << *$3 << " not supported.";
 	exit(1);
       }