Merge pull request #117 from MartinNowack/llvm_raw_ostream

Refactor std::ostreams to llvm::raw_ostream and minor cleanups

51 files changed, 479 insertions, 459 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 720488cc..824fbed5 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -32,7 +32,7 @@ namespace klee {
   class PTreeNode;
   struct InstructionInfo;
 
-std::ostream &operator<<(std::ostream &os, const MemoryMap &mm);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
 
 struct StackFrame {
   KInstIterator caller;
@@ -137,7 +137,7 @@ public:
   }
 
   bool merge(const ExecutionState &b);
-  void dumpStack(std::ostream &out) const;
+  void dumpStack(llvm::raw_ostream &out) const;
 };
 
 }
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index a302591a..c78cd690 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -17,13 +17,15 @@
 #include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/SmallVector.h"
+#include "llvm/Support/raw_ostream.h"
 
+#include <sstream>
 #include <set>
 #include <vector>
-#include <iosfwd> // FIXME: Remove this!!!
 
 namespace llvm {
   class Type;
+  class raw_ostream;
 }
 
 namespace klee {
@@ -181,7 +183,7 @@ public:
   virtual unsigned getNumKids() const = 0;
   virtual ref<Expr> getKid(unsigned i) const = 0;
     
-  virtual void print(std::ostream &os) const;
+  virtual void print(llvm::raw_ostream &os) const;
 
   /// dump - Print the expression to stderr.
   void dump() const;
@@ -221,8 +223,8 @@ public:
 
   /* Static utility methods */
 
-  static void printKind(std::ostream &os, Kind k);
-  static void printWidth(std::ostream &os, Expr::Width w);
+  static void printKind(llvm::raw_ostream &os, Kind k);
+  static void printWidth(llvm::raw_ostream &os, Expr::Width w);
 
   /// returns the smallest number of bytes in which the given width fits
   static inline unsigned getMinBytesForWidth(Width w) {
@@ -291,15 +293,34 @@ inline bool operator>=(const Expr &lhs, const Expr &rhs) {
 
 // Printing operators
 
-inline std::ostream &operator<<(std::ostream &os, const Expr &e) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) {
   e.print(os);
   return os;
 }
 
-inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) {
+// XXX the following macro is to work around the ExprTest unit test compile error
+#ifndef LLVM_29_UNITTEST
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) {
   Expr::printKind(os, kind);
   return os;
 }
+#endif
+
+inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) {
+  std::string str;
+  llvm::raw_string_ostream TmpStr(str);
+  e.print(TmpStr);
+  os << TmpStr.str();
+  return os;
+}
+
+inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kind) {
+  std::string str;
+  llvm::raw_string_ostream TmpStr(str);
+  Expr::printKind(TmpStr, kind);
+  os << TmpStr.str();
+  return os;
+}
 
 // Terminal Exprs
 
diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h
index 63e49dbb..1494aa76 100644
--- a/include/klee/Internal/ADT/TreeStream.h
+++ b/include/klee/Internal/ADT/TreeStream.h
@@ -11,7 +11,6 @@
 #define __UTIL_TREESTREAM_H__
 
 #include <string>
-#include <iostream>
 #include <vector>
 
 namespace klee {
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index e93284d6..abd454b1 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -19,6 +19,8 @@ struct KTest;
 namespace llvm {
 class Function;
 class Module;
+class raw_ostream;
+class raw_fd_ostream;
 }
 
 namespace klee {
@@ -31,10 +33,10 @@ public:
   InterpreterHandler() {}
   virtual ~InterpreterHandler() {}
 
-  virtual std::ostream &getInfoStream() const = 0;
+  virtual llvm::raw_ostream &getInfoStream() const = 0;
 
   virtual std::string getOutputFilename(const std::string &filename) = 0;
-  virtual std::ostream *openOutputFile(const std::string &filename) = 0;
+  virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0;
 
   virtual void incPathsExplored() = 0;
 
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index cf4ebb18..622b0e80 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -12,6 +12,9 @@
 
 #include "klee/Expr.h"
 
+namespace llvm {
+  class raw_ostream;
+}
 namespace klee {
   class ConstraintManager;
 
@@ -20,7 +23,7 @@ namespace klee {
     ExprPPrinter() {}
     
   public:
-    static ExprPPrinter *create(std::ostream &os);
+    static ExprPPrinter *create(llvm::raw_ostream &os);
 
     virtual ~ExprPPrinter() {}
 
@@ -45,7 +48,7 @@ namespace klee {
 
     /// printOne - Pretty print a single expression prefixed by a
     /// message and followed by a line break.
-    static void printOne(std::ostream &os, const char *message, 
+    static void printOne(llvm::raw_ostream &os, const char *message,
                          const ref<Expr> &e);
 
     /// printSingleExpr - Pretty print a single expression.
@@ -55,12 +58,12 @@ namespace klee {
     /// Note that if the output stream is not positioned at the
     /// beginning of a line then printing will not resume at the
     /// correct position following any output line breaks.
-    static void printSingleExpr(std::ostream &os, const ref<Expr> &e);
+    static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e);
 
-    static void printConstraints(std::ostream &os,
+    static void printConstraints(llvm::raw_ostream &os,
                                  const ConstraintManager &constraints);
 
-    static void printQuery(std::ostream &os,
+    static void printQuery(llvm::raw_ostream &os,
                            const ConstraintManager &constraints,
                            const ref<Expr> &q,
                            const ref<Expr> *evalExprsBegin = 0,
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 42f38007..8b072242 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -11,7 +11,6 @@
 #ifndef KLEE_EXPRSMTLIBPRINTER_H
 #define KLEE_EXPRSMTLIBPRINTER_H
 
-#include <ostream>
 #include <string>
 #include <set>
 #include <map>
@@ -20,6 +19,10 @@
 #include <klee/util/PrintContext.h>
 #include <klee/Solver.h>
 
+namespace llvm {
+class raw_ostream;
+}
+
 namespace klee {
 
 /// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic.
@@ -121,7 +124,7 @@ public:
 
   /// Set the output stream that will be printed to.
   /// This call is persistent across queries.
-  void setOutput(std::ostream &output);
+  void setOutput(llvm::raw_ostream &output);
 
   /// Set the query to print. This will setArrayValuesToGet()
   /// to none (i.e. no array values will be requested using
@@ -130,7 +133,7 @@ public:
 
   virtual ~ExprSMTLIBPrinter();
 
-  /// Print the query to the std::ostream
+  /// Print the query to the llvm::raw_ostream
   /// setOutput() and setQuery() must be called before calling this.
   ///
   /// All options should be set before calling this.
@@ -202,7 +205,7 @@ protected:
   std::set<const Array *> usedArrays;
 
   /// Output stream to write to
-  std::ostream *o;
+  llvm::raw_ostream *o;
 
   /// The query to print
   const Query *query;
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
index a9e91925..6b1ef77a 100644
--- a/include/klee/util/PrintContext.h
+++ b/include/klee/util/PrintContext.h
@@ -1,14 +1,14 @@
 #ifndef PRINTCONTEXT_H_
 #define PRINTCONTEXT_H_
 
-#include <ostream>
+#include "klee/Expr.h"
+#include "llvm/Support/raw_ostream.h"
 #include <sstream>
 #include <string>
 #include <stack>
-#include <iomanip>
 
 /// PrintContext - Helper class for pretty printing.
-/// It provides a basic wrapper around std::ostream that keeps track of
+/// It provides a basic wrapper around llvm::raw_ostream that keeps track of
 /// how many characters have been used on the current line.
 ///
 /// It also provides an optional way keeping track of the various levels of indentation
@@ -16,8 +16,7 @@
 /// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
 class PrintContext {
 private:
-  std::ostream &os;
-  std::stringstream ss;
+  llvm::raw_ostream &os;
   std::string newline;
 
   ///This is used to keep track of the stack of indentations used by
@@ -30,7 +29,7 @@ public:
   /// Number of characters on the current line.
   unsigned pos;
 
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
   {
 	  indentStack.push(pos);
   }
@@ -42,7 +41,7 @@ public:
   void breakLine(unsigned indent=0) {
     os << newline;
     if (indent)
-      os << std::setw(indent) << ' ';
+      os.indent(indent) << ' ';
     pos = indent;
   }
 
@@ -79,7 +78,8 @@ public:
 
   template <typename T>
   PrintContext &operator<<(T elt) {
-    ss.str("");
+    std::string str;
+    llvm::raw_string_ostream ss(str);
     ss << elt;
     write(ss.str());
     return *this;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index d14de471..c77149aa 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -20,6 +20,10 @@ using llvm::dyn_cast_or_null;
 #include <assert.h>
 #include <iosfwd> // FIXME: Remove this!!!
 
+namespace llvm {
+  class raw_ostream;
+}
+
 namespace klee {
 
 template<class T>
@@ -107,7 +111,13 @@ public:
 };
 
 template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) {
+  os << *e;
+  return os;
+}
+
+template<class T>
+inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
   os << *e;
   return os;
 }
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index c0d0ef61..59790551 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -10,9 +10,9 @@
 /*
  * This file groups declarations that are common to both KLEE and Kleaver.
  */
-#include <iostream>
 #include "klee/Common.h"
 #include "klee/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
 namespace klee
 {
@@ -29,8 +29,8 @@ namespace klee
 		solver = createPCLoggingSolver(solver,
 					       baseSolverQueryPCLogPath,
 					       MinQueryTimeToLog);
-		std::cerr << "Logging queries that reach solver in .pc format to " 
-			  << baseSolverQueryPCLogPath.c_str() << std::endl;
+		llvm::errs() << "Logging queries that reach solver in .pc format to "
+			  << baseSolverQueryPCLogPath.c_str() << "\n";
 	  }
 
 	  if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB))
@@ -38,8 +38,8 @@ namespace klee
 		solver = createSMTLIBLoggingSolver(solver,
 						   baseSolverQuerySMT2LogPath,
 						   MinQueryTimeToLog);
-		std::cerr << "Logging queries that reach solver in .smt2 format to " 
-			  << baseSolverQuerySMT2LogPath.c_str() << std::endl;
+		llvm::errs() << "Logging queries that reach solver in .smt2 format to "
+			  << baseSolverQuerySMT2LogPath.c_str() << "\n";
 	  }
 
 	  if (UseFastCexSolver)
@@ -62,16 +62,16 @@ namespace klee
 		solver = createPCLoggingSolver(solver,
 					       queryPCLogPath,
 					       MinQueryTimeToLog);
-		std::cerr << "Logging all queries in .pc format to " 
-			  << queryPCLogPath.c_str() << std::endl;
+		llvm::errs() << "Logging all queries in .pc format to "
+			  << queryPCLogPath.c_str() << "\n";
 	  }
 
 	  if (optionIsSet(queryLoggingOptions, ALL_SMTLIB))
 	  {
 		solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath,
 						   MinQueryTimeToLog);
-		std::cerr << "Logging all queries in .smt2 format to " 
-			  << querySMT2LogPath.c_str() << std::endl;
+		llvm::errs() << "Logging all queries in .smt2 format to "
+			  << querySMT2LogPath.c_str() << "\n";
 	  }
 
 	  return solver;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index b2c2a737..e81c776c 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -23,9 +23,10 @@
 #include "llvm/Function.h"
 #endif
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
-#include <iostream>
 #include <iomanip>
+#include <sstream>
 #include <cassert>
 #include <map>
 #include <set>
@@ -177,7 +178,7 @@ void ExecutionState::removeFnAlias(std::string fn) {
 
 /**/
 
-std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) {
+llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm) {
   os << "{";
   MemoryMap::iterator it = mm.begin();
   MemoryMap::iterator ie = mm.end();
@@ -192,8 +193,8 @@ std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) {
 
 bool ExecutionState::merge(const ExecutionState &b) {
   if (DebugLogStateMerge)
-    std::cerr << "-- attempting merge of A:" 
-               << this << " with B:" << &b << "--\n";
+    llvm::errs() << "-- attempting merge of A:" << this << " with B:" << &b
+                 << "--\n";
   if (pc != b.pc)
     return false;
 
@@ -230,21 +231,24 @@ bool ExecutionState::merge(const ExecutionState &b) {
                       commonConstraints.begin(), commonConstraints.end(),
                       std::inserter(bSuffix, bSuffix.end()));
   if (DebugLogStateMerge) {
-    std::cerr << "\tconstraint prefix: [";
-    for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), 
-           ie = commonConstraints.end(); it != ie; ++it)
-      std::cerr << *it << ", ";
-    std::cerr << "]\n";
-    std::cerr << "\tA suffix: [";
-    for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
-           ie = aSuffix.end(); it != ie; ++it)
-      std::cerr << *it << ", ";
-    std::cerr << "]\n";
-    std::cerr << "\tB suffix: [";
-    for (std::set< ref<Expr> >::iterator it = bSuffix.begin(), 
-           ie = bSuffix.end(); it != ie; ++it)
-      std::cerr << *it << ", ";
-    std::cerr << "]\n";
+    llvm::errs() << "\tconstraint prefix: [";
+    for (std::set<ref<Expr> >::iterator it = commonConstraints.begin(),
+                                        ie = commonConstraints.end();
+         it != ie; ++it)
+      llvm::errs() << *it << ", ";
+    llvm::errs() << "]\n";
+    llvm::errs() << "\tA suffix: [";
+    for (std::set<ref<Expr> >::iterator it = aSuffix.begin(),
+                                        ie = aSuffix.end();
+         it != ie; ++it)
+      llvm::errs() << *it << ", ";
+    llvm::errs() << "]\n";
+    llvm::errs() << "\tB suffix: [";
+    for (std::set<ref<Expr> >::iterator it = bSuffix.begin(),
+                                        ie = bSuffix.end();
+         it != ie; ++it)
+      llvm::errs() << *it << ", ";
+    llvm::errs() << "]\n";
   }
 
   // We cannot merge if addresses would resolve differently in the
@@ -257,9 +261,9 @@ bool ExecutionState::merge(const ExecutionState &b) {
   // and not the other
 
   if (DebugLogStateMerge) {
-    std::cerr << "\tchecking object states\n";
-    std::cerr << "A: " << addressSpace.objects << "\n";
-    std::cerr << "B: " << b.addressSpace.objects << "\n";
+    llvm::errs() << "\tchecking object states\n";
+    llvm::errs() << "A: " << addressSpace.objects << "\n";
+    llvm::errs() << "B: " << b.addressSpace.objects << "\n";
   }
     
   std::set<const MemoryObject*> mutated;
@@ -271,22 +275,22 @@ bool ExecutionState::merge(const ExecutionState &b) {
     if (ai->first != bi->first) {
       if (DebugLogStateMerge) {
         if (ai->first < bi->first) {
-          std::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
+          llvm::errs() << "\t\tB misses binding for: " << ai->first->id << "\n";
         } else {
-          std::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
+          llvm::errs() << "\t\tA misses binding for: " << bi->first->id << "\n";
         }
       }
       return false;
     }
     if (ai->second != bi->second) {
       if (DebugLogStateMerge)
-        std::cerr << "\t\tmutated: " << ai->first->id << "\n";
+        llvm::errs() << "\t\tmutated: " << ai->first->id << "\n";
       mutated.insert(ai->first);
     }
   }
   if (ai!=ae || bi!=be) {
     if (DebugLogStateMerge)
-      std::cerr << "\t\tmappings differ\n";
+      llvm::errs() << "\t\tmappings differ\n";
     return false;
   }
   
@@ -348,7 +352,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
   return true;
 }
 
-void ExecutionState::dumpStack(std::ostream &out) const {
+void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
   unsigned idx = 0;
   const KInstruction *target = prevPC;
   for (ExecutionState::stack_ty::const_reverse_iterator
@@ -357,9 +361,11 @@ void ExecutionState::dumpStack(std::ostream &out) const {
     const StackFrame &sf = *it;
     Function *f = sf.kf->function;
     const InstructionInfo &ii = *target->info;
-    out << "\t#" << idx++ 
-        << " " << std::setw(8) << std::setfill('0') << ii.assemblyLine
-        << " in " << f->getName().str() << " (";
+    out << "\t#" << idx++;
+    std::stringstream AssStream;
+    AssStream << std::setw(8) << std::setfill('0') << ii.assemblyLine;
+    out << AssStream.str();
+    out << " in " << f->getName().str() << " (";
     // Yawn, we could go up and print varargs if we wanted to.
     unsigned index = 0;
     for (Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index abb023eb..3a07138d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -86,8 +86,8 @@
 
 #include <cassert>
 #include <algorithm>
-#include <iostream>
 #include <iomanip>
+#include <iosfwd>
 #include <fstream>
 #include <sstream>
 #include <vector>
@@ -316,7 +316,7 @@ Executor::Executor(const InterpreterOptions &opts,
               assert(false);
               break;
     };
-    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
   }
   else {
     coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
@@ -1105,12 +1105,13 @@ Executor::toConstant(ExecutionState &state,
   bool success = solver->getValue(state, e, value);
   assert(success && "FIXME: Unhandled solver failure");
   (void) success;
-    
-  std::ostringstream os;
-  os << "silently concretizing (reason: " << reason << ") expression " << e 
-     << " to value " << value 
-     << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
-      
+
+  std::string str;
+  llvm::raw_string_ostream os(str);
+  os << "silently concretizing (reason: " << reason << ") expression " << e
+     << " to value " << value << " (" << (*(state.pc)).info->file << ":"
+     << (*(state.pc)).info->line << ")";
+
   if (AllExternalWarnings)
     klee_warning(reason, os.str().c_str());
   else
@@ -1167,7 +1168,7 @@ void Executor::executeGetValue(ExecutionState &state,
 void Executor::stepInstruction(ExecutionState &state) {
   if (DebugPrintInstructions) {
     printFileLine(state, state.pc);
-    std::cerr << std::setw(10) << stats::instructions << " ";
+    llvm::errs().indent(10) << stats::instructions << " ";
     llvm::errs() << *(state.pc->inst) << '\n';
   }
 
@@ -1351,10 +1352,10 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
 
 void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
   const InstructionInfo &ii = *ki->info;
-  if (ii.file != "") 
-    std::cerr << "     " << ii.file << ":" << ii.line << ":";
+  if (ii.file != "")
+    llvm::errs() << "     " << ii.file << ":" << ii.line << ":";
   else
-    std::cerr << "     [no debug info]:";
+    llvm::errs() << "     [no debug info]:";
 }
 
 /// Compute the true target of a function call, resolving LLVM and KLEE aliases
@@ -2624,7 +2625,7 @@ void Executor::run(ExecutionState &initialState) {
   
  dump:
   if (DumpStatesOnHalt && !states.empty()) {
-    std::cerr << "KLEE: halting execution, dumping remaining states\n";
+    llvm::errs() << "KLEE: halting execution, dumping remaining states\n";
     for (std::set<ExecutionState*>::iterator
            it = states.begin(), ie = states.end();
          it != ie; ++it) {
@@ -2638,7 +2639,8 @@ void Executor::run(ExecutionState &initialState) {
 
 std::string Executor::getAddressInfo(ExecutionState &state, 
                                      ref<Expr> address) const{
-  std::ostringstream info;
+  std::string Str;
+  llvm::raw_string_ostream info(Str);
   info << "\taddress: " << address << "\n";
   uint64_t example;
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
@@ -2786,8 +2788,9 @@ void Executor::terminateStateOnError(ExecutionState &state,
     }
     if (!EmitAllErrors)
       klee_message("NOTE: now ignoring this error at this location");
-    
-    std::ostringstream msg;
+
+    std::string MsgString;
+    llvm::raw_string_ostream msg(MsgString);
     msg << "Error: " << message << "\n";
     if (ii.file != "") {
       msg << "File: " << ii.file << "\n";
@@ -2800,7 +2803,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string info_str = info.str();
     if (info_str != "")
       msg << "Info: \n" << info_str;
-    interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
+    interpreterHandler->processTestCase(state, MsgString.c_str(), suffix);
   }
     
   terminateState(state);
@@ -2824,8 +2827,8 @@ void Executor::callExternalFunction(ExecutionState &state,
     return;
   
   if (NoExternals && !okExternals.count(function->getName())) {
-    std::cerr << "KLEE:ERROR: Calling not-OK external function : " 
-              << function->getName().str() << "\n";
+    llvm::errs() << "KLEE:ERROR: Calling not-OK external function : "
+                 << function->getName().str() << "\n";
     terminateStateOnError(state, "externals disallowed", "user.err");
     return;
   }
@@ -2864,7 +2867,9 @@ void Executor::callExternalFunction(ExecutionState &state,
   state.addressSpace.copyOutConcretes();
 
   if (!SuppressExternalWarnings) {
-    std::ostringstream os;
+
+    std::string TmpStr;
+    llvm::raw_string_ostream os(TmpStr);
     os << "calling external: " << function->getName().str() << "(";
     for (unsigned i=0; i<arguments.size(); i++) {
       os << arguments[i];
@@ -2923,7 +2928,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
                                  Expr::getMinBytesForWidth(e->getWidth()));
   ref<Expr> res = Expr::createTempRead(array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
-  std::cerr << "Making symbolic: " << eq << "\n";
+  llvm::errs() << "Making symbolic: " << eq << "\n";
   state.addConstraint(eq);
   return res;
 }
@@ -3035,7 +3040,9 @@ void Executor::executeAlloc(ExecutionState &state,
         }
         
         if (hugeSize.second) {
-          std::ostringstream info;
+
+          std::string Str;
+          llvm::raw_string_ostream info(Str);
           ExprPPrinter::printOne(info, "  size expr", size);
           info << "  concretization : " << example << "\n";
           info << "  unbound example: " << tmp << "\n";
@@ -3433,48 +3440,41 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
   return state.symPathOS.getID();
 }
 
-void Executor::getConstraintLog(const ExecutionState &state,
-                                std::string &res,
+void Executor::getConstraintLog(const ExecutionState &state, std::string &res,
                                 Interpreter::LogType logFormat) {
 
   std::ostringstream info;
 
-  switch(logFormat)
-  {
-  case STP:
-  {
-	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  char *log = solver->getConstraintLog(query);
-	  res = std::string(log);
-	  free(log);
-  }
-	  break;
-
-  case KQUERY:
-  {
-	  std::ostringstream info;
-	  ExprPPrinter::printConstraints(info, state.constraints);
-	  res = info.str();
-  }
-	  break;
-
-  case SMTLIB2:
-  {
-	  std::ostringstream info;
-	  ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
-	  printer->setOutput(info);
-	  Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
-	  printer->setQuery(query);
-	  printer->generateOutput();
-	  res = info.str();
-	  delete printer;
-  }
-	  break;
+  switch (logFormat) {
+  case STP: {
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+    char *log = solver->getConstraintLog(query);
+    res = std::string(log);
+    free(log);
+  } break;
+
+  case KQUERY: {
+    std::string Str;
+    llvm::raw_string_ostream info(Str);
+    ExprPPrinter::printConstraints(info, state.constraints);
+    res = info.str();
+  } break;
+
+  case SMTLIB2: {
+    std::string Str;
+    llvm::raw_string_ostream info(Str);
+    ExprSMTLIBPrinter *printer = createSMTLIBPrinter();
+    printer->setOutput(info);
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
+    printer->setQuery(query);
+    printer->generateOutput();
+    res = info.str();
+    delete printer;
+  } break;
 
   default:
-	  klee_warning("Executor::getConstraintLog() : Log format not supported!");
+    klee_warning("Executor::getConstraintLog() : Log format not supported!");
   }
-
 }
 
 bool Executor::getSymbolicSolution(const ExecutionState &state,
@@ -3509,8 +3509,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   solver->setTimeout(0);
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
-    ExprPPrinter::printQuery(std::cerr,
-                             state.constraints, 
+    ExprPPrinter::printQuery(llvm::errs(), state.constraints,
                              ConstantExpr::alloc(0, Expr::Bool));
     return false;
   }
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 06fd4be7..e4622d85 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -53,7 +53,7 @@ public:
   ~HaltTimer() {}
 
   void run() {
-    std::cerr << "KLEE: HaltTimer invoked\n";
+    llvm::errs() << "KLEE: HaltTimer invoked\n";
     executor->setHaltExecution(true);
   }
 };
@@ -122,7 +122,7 @@ void Executor::processTimers(ExecutionState *current,
     if (dumpPTree) {
       char name[32];
       sprintf(name, "ptree%08d.dot", (int) stats::instructions);
-      std::ostream *os = interpreterHandler->openOutputFile(name);
+      llvm::raw_ostream *os = interpreterHandler->openOutputFile(name);
       if (os) {
         processTree->dump(*os);
         delete os;
@@ -132,7 +132,7 @@ void Executor::processTimers(ExecutionState *current,
     }
 
     if (dumpStates) {
-      std::ostream *os = interpreterHandler->openOutputFile("states.txt");
+      llvm::raw_ostream *os = interpreterHandler->openOutputFile("states.txt");
       
       if (os) {
         for (std::set<ExecutionState*>::const_iterator it = states.begin(), 
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 0d828ec4..f6b3dd5e 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -41,7 +41,6 @@
 #include "llvm/Support/CallSite.h"
 
 
-#include <iostream>
 #include <cassert>
 
 using namespace klee;
@@ -62,7 +61,7 @@ namespace klee {
     switch (ce->getOpcode()) {
     default :
       ce->dump();
-      std::cerr << "error: unknown ConstantExpr type\n"
+      llvm::errs() << "error: unknown ConstantExpr type\n"
                 << "opcode: " << ce->getOpcode() << "\n";
       abort();
 
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 2dc16767..4c1e2b86 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -42,7 +42,6 @@
 #endif
 #include <setjmp.h>
 #include <signal.h>
-#include <iostream>
 
 using namespace llvm;
 using namespace klee;
@@ -92,7 +91,7 @@ ExternalDispatcher::ExternalDispatcher() {
   std::string error;
   executionEngine = ExecutionEngine::createJIT(dispatchModule, &error);
   if (!executionEngine) {
-    std::cerr << "unable to make jit: " << error << "\n";
+    llvm::errs() << "unable to make jit: " << error << "\n";
     abort();
   }
 
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 56c1d1a9..c8342df1 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -18,7 +18,6 @@
 
 #include "klee/util/ExprUtil.h"
 
-#include <iostream>
 #include <map>
 #include <set>
 
@@ -246,7 +245,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
     } else {
       if (it!=found.end()) {
         ref<Expr> binding = it->second;
-        std::cerr << "checkForImpliedValues: " << e  << " = " << value << "\n"
+        llvm::errs() << "checkForImpliedValues: " << e  << " = " << value << "\n"
                   << "\t\t implies " << var << " == " << binding
                   << " (error)\n";
         assert(0);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 4bcdd9f7..b6f225d1 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -32,7 +32,6 @@
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
-#include <iostream>
 #include <cassert>
 #include <sstream>
 
@@ -585,23 +584,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) {
 }
 
 void ObjectState::print() {
-  std::cerr << "-- ObjectState --\n";
-  std::cerr << "\tMemoryObject ID: " << object->id << "\n";
-  std::cerr << "\tRoot Object: " << updates.root << "\n";
-  std::cerr << "\tSize: " << size << "\n";
+  llvm::errs() << "-- ObjectState --\n";
+  llvm::errs() << "\tMemoryObject ID: " << object->id << "\n";
+  llvm::errs() << "\tRoot Object: " << updates.root << "\n";
+  llvm::errs() << "\tSize: " << size << "\n";
 
-  std::cerr << "\tBytes:\n";
+  llvm::errs() << "\tBytes:\n";
   for (unsigned i=0; i<size; i++) {
-    std::cerr << "\t\t["<<i<<"]"
+    llvm::errs() << "\t\t["<<i<<"]"
                << " concrete? " << isByteConcrete(i)
                << " known-sym? " << isByteKnownSymbolic(i)
                << " flushed? " << isByteFlushed(i) << " = ";
     ref<Expr> e = read8(i);
-    std::cerr << e << "\n";
+    llvm::errs() << e << "\n";
   }
 
-  std::cerr << "\tUpdates:\n";
+  llvm::errs() << "\tUpdates:\n";
   for (const UpdateNode *un=updates.head; un; un=un->next) {
-    std::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
+    llvm::errs() << "\t\t[" << un->index << "] = " << un->value << "\n";
   }
 }
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 349761cd..f0e7ab51 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -13,7 +13,6 @@
 #include <klee/util/ExprPPrinter.h>
 
 #include <vector>
-#include <iostream>
 
 using namespace klee;
 
@@ -51,7 +50,7 @@ void PTree::remove(Node *n) {
   } while (n && !n->left && !n->right);
 }
 
-void PTree::dump(std::ostream &os) {
+void PTree::dump(llvm::raw_ostream &os) {
   ExprPPrinter *pp = ExprPPrinter::create(os);
   pp->setNewline("\\l");
   os << "digraph G {\n";
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index 6accc8e2..11d3f48c 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -12,10 +12,6 @@
 
 #include <klee/Expr.h>
 
-#include <utility>
-#include <cassert>
-#include <iostream>
-
 namespace klee {
   class ExecutionState;
 
@@ -34,7 +30,7 @@ namespace klee {
                                  const data_type &rightData);
     void remove(Node *n);
 
-    void dump(std::ostream &os);
+    void dump(llvm::raw_ostream &os);
   };
 
   class PTreeNode {
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 8c3e26bc..2610f17e 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -411,17 +411,17 @@ ExecutionState &MergingSearcher::selectState() {
   }
   
   if (DebugLogMerge)
-    std::cerr << "-- all at merge --\n";
+    llvm::errs() << "-- all at merge --\n";
   for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
          it = merges.begin(), ie = merges.end(); it != ie; ++it) {
     if (DebugLogMerge) {
-      std::cerr << "\tmerge: " << it->first << " [";
+      llvm::errs() << "\tmerge: " << it->first << " [";
       for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
              ie2 = it->second.end(); it2 != ie2; ++it2) {
         ExecutionState *state = *it2;
-        std::cerr << state << ", ";
+        llvm::errs() << state << ", ";
       }
-      std::cerr << "]\n";
+      llvm::errs() << "]\n";
     }
 
     // merge states
@@ -440,13 +440,13 @@ ExecutionState &MergingSearcher::selectState() {
         }
       }
       if (DebugLogMerge && !toErase.empty()) {
-        std::cerr << "\t\tmerged: " << base << " with [";
+        llvm::errs() << "\t\tmerged: " << base << " with [";
         for (std::set<ExecutionState*>::iterator it = toErase.begin(),
                ie = toErase.end(); it != ie; ++it) {
-          if (it!=toErase.begin()) std::cerr << ", ";
-          std::cerr << *it;
+          if (it!=toErase.begin()) llvm::errs() << ", ";
+          llvm::errs() << *it;
         }
-        std::cerr << "]\n";
+        llvm::errs() << "]\n";
       }
       for (std::set<ExecutionState*>::iterator it = toErase.begin(),
              ie = toErase.end(); it != ie; ++it) {
@@ -464,7 +464,7 @@ ExecutionState &MergingSearcher::selectState() {
   }
   
   if (DebugLogMerge)
-    std::cerr << "-- merge complete, continuing --\n";
+    llvm::errs() << "-- merge complete, continuing --\n";
   
   return selectState();
 }
@@ -512,7 +512,8 @@ ExecutionState &BatchingSearcher::selectState() {
     if (lastState) {
       double delta = util::getWallTime()-lastStartTime;
       if (delta>timeBudget*1.1) {
-        std::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
+        llvm::errs() << "KLEE: increased time budget from " << timeBudget
+                     << " to " << delta << "\n";
         timeBudget = delta;
       }
     }
@@ -578,7 +579,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
 
   if (baseSearcher->empty()) {
     time *= 2;
-    std::cerr << "KLEE: increasing time budget to: " << time << "\n";
+    llvm::errs() << "KLEE: increasing time budget to: " << time << "\n";
     baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
     pausedStates.clear();
   }
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 3944d4b4..d866f521 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,18 +10,17 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "llvm/Support/raw_ostream.h"
 #include <vector>
 #include <set>
 #include <map>
 #include <queue>
 
-// FIXME: Move out of header, use llvm streams.
-#include <ostream>
-
 namespace llvm {
   class BasicBlock;
   class Function;
   class Instruction;
+  class raw_ostream;
 }
 
 namespace klee {
@@ -43,7 +42,7 @@ namespace klee {
 
     // prints name of searcher as a klee_message()
     // TODO: could probably make prettier or more flexible
-    virtual void printName(std::ostream &os) { 
+    virtual void printName(llvm::raw_ostream &os) {
       os << "<unnamed searcher>\n";
     }
 
@@ -90,7 +89,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return states.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "DFSSearcher\n";
     }
   };
@@ -104,7 +103,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return states.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "BFSSearcher\n";
     }
   };
@@ -118,7 +117,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return states.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "RandomSearcher\n";
     }
   };
@@ -150,7 +149,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty();
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "WeightedRandomSearcher::";
       switch(type) {
       case Depth              : os << "Depth\n"; return;
@@ -176,7 +175,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty();
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "RandomPathSearcher\n";
     }
   };
@@ -199,7 +198,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "MergingSearcher\n";
     }
   };
@@ -222,7 +221,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "BumpMergingSearcher\n";
     }
   };
@@ -247,7 +246,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return baseSearcher->empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "<BatchingSearcher> timeBudget: " << timeBudget
          << ", instructionBudget: " << instructionBudget
          << ", baseSearcher:\n";
@@ -270,7 +269,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return baseSearcher->empty() && pausedStates.empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "IterativeDeepeningTimeSearcher\n";
     }
   };
@@ -290,7 +289,7 @@ namespace klee {
                 const std::set<ExecutionState*> &addedStates,
                 const std::set<ExecutionState*> &removedStates);
     bool empty() { return searchers[0]->empty(); }
-    void printName(std::ostream &os) {
+    void printName(llvm::raw_ostream &os) {
       os << "<InterleavedSearcher> containing "
          << searchers.size() << " searchers:\n";
       for (searchers_ty::iterator it = searchers.begin(), ie = searchers.end();
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index ca9f7b63..a7a1b32e 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -27,6 +27,7 @@
 #include "llvm/Module.h"
 #endif
 #include "llvm/ADT/Twine.h"
+#include "llvm/Support/Debug.h"
 
 #include <errno.h>
 
@@ -251,7 +252,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state,
 
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    std::cerr << "TAINT: skipping abort fail\n";
+    llvm::errs() << "TAINT: skipping abort fail\n";
     executor.terminateState(state);
   } else {
     executor.terminateStateOnError(state, "abort failure", "abort.err");
@@ -279,7 +280,8 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
          "invalid number of arguments to klee_alias_function");
   std::string old_fn = readStringAtAddress(state, arguments[0]);
   std::string new_fn = readStringAtAddress(state, arguments[1]);
-  //std::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
+  DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn
+                                           << "() with " << new_fn << "()\n");
   if (old_fn == new_fn)
     state.removeFnAlias(old_fn);
   else state.addFnAlias(old_fn, new_fn);
@@ -292,8 +294,8 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    std::cerr << "TAINT: skipping assertion:" 
-               << readStringAtAddress(state, arguments[0]) << "\n";
+    llvm::errs() << "TAINT: skipping assertion:"
+                 << readStringAtAddress(state, arguments[0]) << "\n";
     executor.terminateState(state);
   } else
     executor.terminateStateOnError(state, 
@@ -308,8 +310,8 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    std::cerr << "TAINT: skipping assertion:" 
-               << readStringAtAddress(state, arguments[0]) << "\n";
+    llvm::errs() << "TAINT: skipping assertion:"
+                 << readStringAtAddress(state, arguments[0]) << "\n";
     executor.terminateState(state);
   } else
     executor.terminateStateOnError(state, 
@@ -326,9 +328,9 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    std::cerr << "TAINT: skipping klee_report_error:"
-               << readStringAtAddress(state, arguments[2]) << ":"
-               << readStringAtAddress(state, arguments[3]) << "\n";
+    llvm::errs() << "TAINT: skipping klee_report_error:"
+                 << readStringAtAddress(state, arguments[2]) << ":"
+                 << readStringAtAddress(state, arguments[3]) << "\n";
     executor.terminateState(state);
   } else
     executor.terminateStateOnError(state, 
@@ -444,7 +446,7 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
          "invalid number of arguments to klee_print_expr");
 
   std::string msg_str = readStringAtAddress(state, arguments[0]);
-  std::cerr << msg_str << ":" << arguments[1] << "\n";
+  llvm::errs() << msg_str << ":" << arguments[1] << "\n";
 }
 
 void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
@@ -466,7 +468,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
 void SpecialFunctionHandler::handleStackTrace(ExecutionState &state,
                                               KInstruction *target,
                                               std::vector<ref<Expr> > &arguments) {
-  state.dumpStack(std::cout);
+  state.dumpStack(outs());
 }
 
 void SpecialFunctionHandler::handleWarning(ExecutionState &state,
@@ -497,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
          "invalid number of arguments to klee_print_range");
 
   std::string msg_str = readStringAtAddress(state, arguments[0]);
-  std::cerr << msg_str << ":" << arguments[1];
+  llvm::errs() << msg_str << ":" << arguments[1];
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
@@ -509,15 +511,15 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
                                           res);
     assert(success && "FIXME: Unhandled solver failure");
     if (res) {
-      std::cerr << " == " << value;
+      llvm::errs() << " == " << value;
     } else { 
-      std::cerr << " ~= " << value;
+      llvm::errs() << " ~= " << value;
       std::pair< ref<Expr>, ref<Expr> > res =
         executor.solver->getRange(state, arguments[1]);
-      std::cerr << " (in [" << res.first << ", " << res.second <<"])";
+      llvm::errs() << " (in [" << res.first << ", " << res.second <<"])";
     }
   }
-  std::cerr << "\n";
+  llvm::errs() << "\n";
 }
 
 void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 4709a5bc..0946d2ba 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -46,12 +46,10 @@
 #endif
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/CFG.h"
-#include "llvm/Support/raw_os_ostream.h"
 #include "llvm/Support/Process.h"
 #include "llvm/Support/Path.h"
 #include "llvm/Support/FileSystem.h"
 
-#include <iostream>
 #include <fstream>
 #include <unistd.h>
 
@@ -432,11 +430,12 @@ void StatsTracker::updateStateStatistics(uint64_t addend) {
 void StatsTracker::writeIStats() {
   Module *m = executor.kmodule->module;
   uint64_t istatsMask = 0;
-  std::ostream &of = *istatsFile;
+  llvm::raw_fd_ostream &of = *istatsFile;
   
-  of.seekp(0, std::ios::end);
-  unsigned istatsSize = of.tellp();
-  of.seekp(0);
+  // We assume that we didn't move the file pointer
+  unsigned istatsSize = of.tell();
+
+  of.seek(0);
 
   of << "version: 1\n";
   of << "creator: klee\n";
@@ -564,7 +563,7 @@ void StatsTracker::writeIStats() {
     updateStateStatistics((uint64_t)-1);
   
   // Clear then end of the file if necessary (no truncate op?).
-  unsigned pos = of.tellp();
+  unsigned pos = of.tell();
   for (unsigned i=pos; i<istatsSize; ++i)
     of << '\n';
   
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index 8f3a01a2..629a723d 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -12,13 +12,13 @@
 
 #include "CallPathManager.h"
 
-#include <iostream>
 #include <set>
 
 namespace llvm {
   class BranchInst;
   class Function;
   class Instruction;
+  class raw_fd_ostream;
 }
 
 namespace klee {
@@ -36,7 +36,7 @@ namespace klee {
     Executor &executor;
     std::string objectFilename;
 
-    std::ostream *statsFile, *istatsFile;
+    llvm::raw_fd_ostream *statsFile, *istatsFile;
     double startWallTime;
     
     unsigned numBranches;
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 2c75f796..72f3351f 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -129,7 +129,7 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
     searcher = new IterativeDeepeningTimeSearcher(searcher);
   }
 
-  std::ostream &os = executor.getHandler().getInfoStream();
+  llvm::raw_ostream &os = executor.getHandler().getInfoStream();
 
   os << "BEGIN searcher description\n";
   searcher->printName(os);
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 90d9bcd4..ae4563f4 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -19,7 +19,6 @@
 #include "llvm/Support/CommandLine.h"
 #include "klee/Internal/Module/KModule.h"
 
-#include <iostream>
 #include <map>
 
 using namespace klee;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 82c60205..d54b8f4d 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -14,13 +14,13 @@
 #include "llvm/ADT/Hashing.h"
 #endif
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 // FIXME: We shouldn't need this once fast constant support moves into
 // Core. If we need to do arithmetic, we probably want to use APInt.
 #include "klee/Internal/Support/IntEvaluation.h"
 
 #include "klee/util/ExprPPrinter.h"
 
-#include <iostream>
 #include <sstream>
 
 using namespace klee;
@@ -116,7 +116,7 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
   return 0;
 }
 
-void Expr::printKind(std::ostream &os, Kind k) {
+void Expr::printKind(llvm::raw_ostream &os, Kind k) {
   switch(k) {
 #define X(C) case C: os << #C; break
     X(Constant);
@@ -286,7 +286,7 @@ ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
 }
 
 
-void Expr::printWidth(std::ostream &os, Width width) {
+void Expr::printWidth(llvm::raw_ostream &os, Width width) {
   switch(width) {
   case Expr::Bool: os << "Expr::Bool"; break;
   case Expr::Int8: os << "Expr::Int8"; break;
@@ -306,13 +306,13 @@ ref<Expr> Expr::createIsZero(ref<Expr> e) {
   return EqExpr::create(e, ConstantExpr::create(0, e->getWidth()));
 }
 
-void Expr::print(std::ostream &os) const {
+void Expr::print(llvm::raw_ostream &os) const {
   ExprPPrinter::printSingleExpr(os, const_cast<Expr*>(this));
 }
 
 void Expr::dump() const {
-  this->print(std::cerr);
-  std::cerr << std::endl;
+  this->print(errs());
+  errs() << "\n";
 }
 
 /***/
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index d58358b5..ddcc57a1 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -13,12 +13,10 @@
 #include "klee/Constraints.h"
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <map>
 #include <vector>
-#include <iostream>
-#include <sstream>
-#include <iomanip>
 
 using namespace klee;
 
@@ -47,7 +45,7 @@ private:
   std::map<const UpdateNode*, unsigned> updateBindings;
   std::set< ref<Expr> > couldPrint, shouldPrint;
   std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
-  std::ostream &os;
+  llvm::raw_ostream &os;
   unsigned counter;
   unsigned updateCounter;
   bool hasScan;
@@ -300,7 +298,7 @@ private:
   }
 
 public:
-  PPrinter(std::ostream &_os) : os(_os), newline("\n") {
+  PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") {
     reset();
   }
 
@@ -426,11 +424,11 @@ public:
   }
 };
 
-ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) {
+ExprPPrinter *klee::ExprPPrinter::create(llvm::raw_ostream &os) {
   return new PPrinter(os);
 }
 
-void ExprPPrinter::printOne(std::ostream &os,
+void ExprPPrinter::printOne(llvm::raw_ostream &os,
                             const char *message, 
                             const ref<Expr> &e) {
   PPrinter p(os);
@@ -444,7 +442,7 @@ void ExprPPrinter::printOne(std::ostream &os,
   PC.breakLine();
 }
 
-void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
+void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) {
   PPrinter p(os);
   p.scan(e);
 
@@ -454,13 +452,13 @@ void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
   p.print(e, PC);
 }
 
-void ExprPPrinter::printConstraints(std::ostream &os,
+void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
                                     const ConstraintManager &constraints) {
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
 
-void ExprPPrinter::printQuery(std::ostream &os,
+void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const ConstraintManager &constraints,
                               const ref<Expr> &q,
                               const ref<Expr> *evalExprsBegin,
diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp
index 6a88ab5d..d4243452 100644
--- a/lib/Expr/ExprSMTLIBLetPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -8,12 +8,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include <iostream>
+#include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/CommandLine.h"
 #include "klee/util/ExprSMTLIBLetPrinter.h"
 
-using namespace std;
-
 namespace ExprSMTLIBOptions {
 llvm::cl::opt<bool>
 useLetExpressions("smtlib-use-let-expressions",
@@ -31,7 +29,7 @@ ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter()
 
 void ExprSMTLIBLetPrinter::generateOutput() {
   if (p == NULL || query == NULL || o == NULL) {
-    std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
+    llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n";
     return;
   }
 
@@ -85,7 +83,7 @@ void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) {
 void ExprSMTLIBLetPrinter::generateBindings() {
   // Assign a number to each binding that will be used
   unsigned int counter = 0;
-  for (set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
+  for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
        i != twoOrMoreEO.end(); ++i) {
     bindings.insert(std::make_pair(*i, counter));
     ++counter;
@@ -94,7 +92,7 @@ void ExprSMTLIBLetPrinter::generateBindings() {
 
 void ExprSMTLIBLetPrinter::printExpression(
     const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
-  map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
+  std::map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
 
   if (disablePrintedAbbreviations || i == bindings.end()) {
     /*There is no abbreviation for this expression so print it normally.
@@ -143,7 +141,7 @@ void ExprSMTLIBLetPrinter::printLetExpression() {
     p->pushIndent();
 
     // Print each binding
-    for (map<const ref<Expr>, unsigned int>::const_iterator i =
+    for (std::map<const ref<Expr>, unsigned int>::const_iterator i =
              bindings.begin();
          i != bindings.end(); ++i) {
       printSeperator();
@@ -173,7 +171,8 @@ void ExprSMTLIBLetPrinter::printLetExpression() {
   // print out Expressions with abbreviations.
   unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
   unsigned int itemsLeft = numberOfItems;
-  vector<ref<Expr> >::const_iterator constraint = query->constraints.begin();
+  std::vector<ref<Expr> >::const_iterator constraint =
+      query->constraints.begin();
 
   /* Produce nested (and () () statements. If the constraint set
    * is empty then we will only print the "queryAssert".
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index cff5abfe..bbb82d0d 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -1,5 +1,4 @@
-//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++
-//-*-===//
+//===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,14 +6,10 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#include <iostream>
-
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/CommandLine.h"
 #include "klee/util/ExprSMTLIBPrinter.h"
 
-using namespace std;
-
 namespace ExprSMTLIBOptions {
 // Command line options
 llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode>
@@ -53,7 +48,7 @@ ExprSMTLIBPrinter::~ExprSMTLIBPrinter() {
     delete p;
 }
 
-void ExprSMTLIBPrinter::setOutput(std::ostream &output) {
+void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) {
   o = &output;
   if (p != NULL)
     delete p;
@@ -146,8 +141,8 @@ void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) {
     break;
 
   default:
-    std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
-                 "display mode" << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
+                    "display mode\n";
   }
 }
 
@@ -425,8 +420,8 @@ void ExprSMTLIBPrinter::scanAll() {
 
 void ExprSMTLIBPrinter::generateOutput() {
   if (p == NULL || query == NULL || o == NULL) {
-    std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
-                 "Output or query bad!" << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
+                    "Output or query bad!\n";
     return;
   }
 
@@ -451,7 +446,7 @@ void ExprSMTLIBPrinter::printSetLogic() {
     *o << "QF_AUFBV";
     break;
   }
-  *o << " )" << std::endl;
+  *o << " )\n";
 }
 
 namespace {
@@ -467,7 +462,7 @@ struct ArrayPtrsByName {
 void ExprSMTLIBPrinter::printArrayDeclarations() {
   // Assume scan() has been called
   if (humanReadable)
-    *o << "; Array declarations" << endl;
+    *o << "; Array declarations\n";
 
   // Declare arrays in a deterministic order.
   std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
@@ -478,13 +473,13 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
                                             "(Array (_ BitVec "
        << (*it)->getDomain() << ") "
                                 "(_ BitVec " << (*it)->getRange() << ") ) )"
-       << endl;
+       << "\n";
   }
 
   // Set array values for constant values
   if (haveConstantArray) {
     if (humanReadable)
-      *o << "; Constant Array Definitions" << endl;
+      *o << "; Constant Array Definitions\n";
 
     const Array *array;
 
@@ -497,7 +492,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
         /*loop over elements in the array and generate an assert statement
           for each one
          */
-        for (vector<ref<ConstantExpr> >::const_iterator
+        for (std::vector<ref<ConstantExpr> >::const_iterator
                  ce = array->constantValues.begin();
              ce != array->constantValues.end(); ce++, byteIndex++) {
           *p << "(assert (";
@@ -527,7 +522,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
 
 void ExprSMTLIBPrinter::printConstraints() {
   if (humanReadable)
-    *o << "; Constraints" << endl;
+    *o << "; Constraints\n";
 
   // Generate assert statements for each constraint
   for (ConstraintManager::const_iterator i = query->constraints.begin();
@@ -548,7 +543,7 @@ void ExprSMTLIBPrinter::printConstraints() {
 
 void ExprSMTLIBPrinter::printAction() {
   // Ask solver to check for satisfiability
-  *o << "(check-sat)" << endl;
+  *o << "(check-sat)\n";
 
   /* If we has arrays to find the values of then we'll
    * ask the solver for the value of each bitvector in each array
@@ -558,14 +553,14 @@ void ExprSMTLIBPrinter::printAction() {
     const Array *theArray = 0;
 
     // loop over the array names
-    for (vector<const Array *>::const_iterator it =
+    for (std::vector<const Array *>::const_iterator it =
              arraysToCallGetValueOn->begin();
          it != arraysToCallGetValueOn->end(); it++) {
       theArray = *it;
       // Loop over the array indices
       for (unsigned int index = 0; index < theArray->size; ++index) {
         *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " "
-           << theArray->getDomain() << ") ) ) )" << endl;
+           << theArray->getDomain() << ") ) ) )\n";
       }
     }
   }
@@ -573,8 +568,8 @@ void ExprSMTLIBPrinter::printAction() {
 
 void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
   if (e.isNull()) {
-    std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
-              << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
+                 << "\n";
     return;
   }
 
@@ -609,7 +604,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
   }
 }
 
-void ExprSMTLIBPrinter::printExit() { *o << "(exit)" << endl; }
+void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; }
 
 bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) {
   if (l > QF_AUFBV)
@@ -627,7 +622,7 @@ void ExprSMTLIBPrinter::printSeperator() {
 }
 
 void ExprSMTLIBPrinter::printNotice() {
-  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
+  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n";
 }
 
 void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; }
@@ -638,7 +633,7 @@ void ExprSMTLIBPrinter::printOptions() {
            smtlibBoolOptions.begin();
        i != smtlibBoolOptions.end(); i++) {
     *o << "(set-option :" << getSMTLIBOptionString(i->first) << " "
-       << ((i->second) ? "true" : "false") << ")" << endl;
+       << ((i->second) ? "true" : "false") << ")\n";
   }
 }
 
@@ -742,8 +737,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e,
     *p << ")";
 
     if (bitWidth != Expr::Bool)
-      std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
-                << bitWidth << ") to bool!" << std::endl;
+      llvm::errs()
+          << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
+          << bitWidth << ") to bool!\n";
 
   } break;
   default:
@@ -883,7 +879,8 @@ ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) {
    * that the solver knows what to do when we ask for the values of arrays
    * that don't feature in our query!
    */
-  for (vector<const Array *>::const_iterator i = a.begin(); i != a.end(); ++i) {
+  for (std::vector<const Array *>::const_iterator i = a.begin(); i != a.end();
+       ++i) {
     usedArrays.insert(*i);
   }
 }
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
index 9859ff36..e250a968 100644
--- a/lib/Expr/Lexer.cpp
+++ b/lib/Expr/Lexer.cpp
@@ -13,7 +13,6 @@
 #include "llvm/Support/raw_ostream.h"
 
 #include <iomanip>
-#include <iostream>
 #include <string.h>
 
 using namespace llvm;
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 5b3e96b7..aebce666 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -22,7 +22,6 @@
 #include "llvm/Support/raw_ostream.h"
 
 #include <cassert>
-#include <iostream>
 #include <map>
 #include <cstring>
 
@@ -1522,7 +1521,7 @@ void ParserImpl::Error(const char *Message, const Token &At) {
   if (MaxErrors && NumErrors >= MaxErrors)
     return;
 
-  std::cerr << Filename
+  llvm::errs() << Filename
             << ":" << At.line << ":" << At.column 
             << ": error: " << Message << "\n";
 
@@ -1544,18 +1543,18 @@ void ParserImpl::Error(const char *Message, const Token &At) {
     ++LineEnd;
 
   // Show the line.
-  std::cerr << std::string(LineBegin, LineEnd) << "\n";
+  llvm::errs() << std::string(LineBegin, LineEnd) << "\n";
 
   // Show the caret or squiggly, making sure to print back spaces the
   // same.
   for (const char *S=LineBegin; S != At.start; ++S)
-    std::cerr << (isspace(*S) ? *S : ' ');
+    llvm::errs() << (isspace(*S) ? *S : ' ');
   if (At.length > 1) {
     for (unsigned i=0; i<At.length; ++i)
-      std::cerr << '~';
+      llvm::errs() << '~';
   } else
-    std::cerr << '^';
-  std::cerr << '\n';
+    llvm::errs() << '^';
+  llvm::errs() << '\n';
 }
 
 // AST API
@@ -1564,20 +1563,20 @@ void ParserImpl::Error(const char *Message, const Token &At) {
 Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
-  std::cout << "array " << Root->name
+  llvm::outs() << "array " << Root->name
             << "[" << Root->size << "]"
             << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
   if (Root->isSymbolicArray()) {
-    std::cout << "symbolic\n";
+    llvm::outs() << "symbolic\n";
   } else {
-    std::cout << '[';
+    llvm::outs() << '[';
     for (unsigned i = 0, e = Root->size; i != e; ++i) {
       if (i)
-        std::cout << " ";
-      std::cout << Root->constantValues[i];
+        llvm::outs() << " ";
+      llvm::outs() << Root->constantValues[i];
     }
-    std::cout << "]\n";
+    llvm::outs() << "]\n";
   }
 }
 
@@ -1592,7 +1591,7 @@ void QueryCommand::dump() {
     ObjectsBegin = &Objects[0];
     ObjectsEnd = ObjectsBegin + Objects.size();
   }
-  ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), 
+  ExprPPrinter::printQuery(llvm::outs(), ConstraintManager(Constraints),
                            Query, ValuesBegin, ValuesEnd,
                            ObjectsBegin, ObjectsEnd,
                            false);
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 80b6b245..e1076d43 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -46,7 +46,6 @@
 #include "llvm/Transforms/Scalar.h"
 #include "llvm/Transforms/Utils/BasicBlockUtils.h"
 #include "llvm/Support/CallSite.h"
-#include <iostream>
 
 using namespace llvm;
 using namespace klee;
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index e06e722a..697b6ea9 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -430,15 +430,13 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   // around a kcachegrind parsing bug (it puts them on new lines), so
   // that source browsing works.
   if (OutputSource) {
-    std::ostream *os = ih->openOutputFile("assembly.ll");
-    assert(os && os->good() && "unable to open source output");
-
-    llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os);
+    llvm::raw_fd_ostream *os = ih->openOutputFile("assembly.ll");
+    assert(os && !os->has_error() && "unable to open source output");
 
     // We have an option for this in case the user wants a .ll they
     // can compile.
     if (NoTruncateSourceLines) {
-      *ros << *module;
+      *os << *module;
     } else {
       std::string string;
       llvm::raw_string_ostream rss(string);
@@ -449,30 +447,26 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
       for (;;) {
         const char *end = index(position, '\n');
         if (!end) {
-          *ros << position;
+          *os << position;
           break;
         } else {
           unsigned count = (end - position) + 1;
           if (count<255) {
-            ros->write(position, count);
+            os->write(position, count);
           } else {
-            ros->write(position, 254);
-            *ros << "\n";
+            os->write(position, 254);
+            *os << "\n";
           }
           position = end+1;
         }
       }
     }
-    delete ros;
-
     delete os;
   }
 
   if (OutputModule) {
-    std::ostream *f = ih->openOutputFile("final.bc");
-    llvm::raw_os_ostream* rfs = new llvm::raw_os_ostream(*f);
-    WriteBitcodeToFile(module, *rfs);
-    delete rfs;
+    llvm::raw_fd_ostream *f = ih->openOutputFile("final.bc");
+    WriteBitcodeToFile(module, *f);
     delete f;
   }
 
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 4f65d0e7..d00cf574 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -28,7 +28,6 @@
 #include "llvm/Object/ObjectFile.h"
 #include "llvm/Object/Error.h"
 #include "llvm/Support/FileSystem.h"
-#include "llvm/Support/raw_os_ostream.h"
 #include "llvm/IR/ValueSymbolTable.h"
 #include "llvm/Support/SourceMgr.h"
 #include "llvm/Support/DataStream.h"
@@ -51,7 +50,6 @@
 
 #include <map>
 #include <set>
-#include <iostream>
 #include <fstream>
 #include <sstream>
 #include <string>
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index 9c200bc8..ed1e0e34 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -40,7 +40,6 @@
 #include "llvm/Transforms/Scalar.h"
 #include "llvm/Support/PassNameParser.h"
 #include "llvm/Support/PluginLoader.h"
-#include <iostream>
 using namespace llvm;
 
 #if 0
@@ -272,7 +271,7 @@ void Optimize(Module* M) {
     if (Opt->getNormalCtor())
       addPass(Passes, Opt->getNormalCtor()());
     else
-      std::cerr << "llvm-ld: cannot create pass: " << Opt->getPassName() 
+      llvm::errs() << "llvm-ld: cannot create pass: " << Opt->getPassName()
                 << "\n";
   }
 #endif
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);
       }
 
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 6e52dc32..57e44806 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -18,7 +18,9 @@
 // FIXME: Use APInt.
 #include "klee/Internal/Support/IntEvaluation.h"
 
-#include <iostream>
+#define DEBUG_TYPE "cex-solver"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/raw_ostream.h"
 #include <sstream>
 #include <cassert>
 #include <map>
@@ -109,7 +111,7 @@ public:
   ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
   ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     if (isFixed()) {
       os << m_min;
     } else {
@@ -283,7 +285,8 @@ public:
   }
 };
 
-inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const ValueRange &vr) {
   vr.print(os);
   return os;
 }
@@ -405,10 +408,6 @@ public:
     : objects(_objects) {}
 };
 
-#if 0
-#define DEBUG
-#endif
-
 class CexData {
 public:
   std::map<const Array*, CexObjectData*> objects;
@@ -442,9 +441,7 @@ public:
   }
 
   void propogatePossibleValues(ref<Expr> e, CexValueData range) {
-    #ifdef DEBUG
-    std::cerr << "propogate: " << range << " for\n" << e << "\n";
-    #endif
+    DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";);
 
     switch (e->getKind()) {
     case Expr::Constant:
@@ -938,27 +935,29 @@ public:
   }
 
   void dump() {
-    std::cerr << "-- propogated values --\n";
-    for (std::map<const Array*, CexObjectData*>::iterator 
-           it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+    llvm::errs() << "-- propogated values --\n";
+    for (std::map<const Array *, CexObjectData *>::iterator
+             it = objects.begin(),
+             ie = objects.end();
+         it != ie; ++it) {
       const Array *A = it->first;
       CexObjectData *COD = it->second;
-    
-      std::cerr << A->name << "\n";
-      std::cerr << "possible: [";
+
+      llvm::errs() << A->name << "\n";
+      llvm::errs() << "possible: [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          std::cerr << ", ";
-        std::cerr << COD->getPossibleValues(i);
+          llvm::errs() << ", ";
+        llvm::errs() << COD->getPossibleValues(i);
       }
-      std::cerr << "]\n";
-      std::cerr << "exact   : [";
+      llvm::errs() << "]\n";
+      llvm::errs() << "exact   : [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          std::cerr << ", ";
-        std::cerr << COD->getExactValues(i);
+          llvm::errs() << ", ";
+        llvm::errs() << COD->getExactValues(i);
       }
-      std::cerr << "]\n";
+      llvm::errs() << "]\n";
     }
   }
 };
@@ -1009,9 +1008,7 @@ static bool propogateValues(const Query& query, CexData &cd,
     cd.propogateExactValue(query.expr, 0);
   }
 
-#ifdef DEBUG
-  cd.dump();
-#endif
+  DEBUG(cd.dump(););
   
   // Check the result.
   bool hasSatisfyingAssignment = true;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index d9fc77dc..46b4ee56 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -15,10 +15,12 @@
 
 #include "klee/util/ExprUtil.h"
 
+#define DEBUG_TYPE "independent-solver"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <vector>
 #include <ostream>
-#include <iostream>
 
 using namespace klee;
 using namespace llvm;
@@ -60,7 +62,7 @@ public:
     return false;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     bool first = true;
     os << "{";
     for (typename set_ty::iterator it = s.begin(), ie = s.end(); 
@@ -76,8 +78,9 @@ public:
   }
 };
 
-template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) {
+template <class T>
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const ::DenseSet<T> &dis) {
   dis.print(os);
   return os;
 }
@@ -124,7 +127,7 @@ public:
     return *this;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     os << "{";
     bool first = true;
     for (std::set<const Array*>::iterator it = wholeObjects.begin(), 
@@ -214,7 +217,8 @@ public:
   }
 };
 
-inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const IndependentElementSet &ies) {
   ies.print(os);
   return os;
 }
@@ -247,20 +251,21 @@ IndependentElementSet getIndependentConstraints(const Query& query,
     worklist.swap(newWorklist);
   } while (!done);
 
-  if (0) {
+DEBUG(
     std::set< ref<Expr> > reqset(result.begin(), result.end());
-    std::cerr << "--\n";
-    std::cerr << "Q: " << query.expr << "\n";
-    std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
+    errs() << "--\n";
+    errs() << "Q: " << query.expr << "\n";
+    errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
     int i = 0;
-  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
-         ie = query.constraints.end(); it != ie; ++it) {
-      std::cerr << "C" << i++ << ": " << *it;
-      std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
-      std::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+        ie = query.constraints.end(); it != ie; ++it) {
+      errs() << "C" << i++ << ": " << *it;
+      errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
+      errs() << "\telts: " << IndependentElementSet(*it) << "\n";
     }
-    std::cerr << "elts closure: " << eltsClosure << "\n";
-  }
+    errs() << "elts closure: " << eltsClosure << "\n";
+ );
+
 
   return eltsClosure;
 }
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index f1e55614..b5c99907 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -599,9 +599,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
     
     ++stats::queryConstructs;
     
-//     std::cerr << "Constructing expression ";
-//     ExprPPrinter::printSingleExpr(std::cerr, e);
-//     std::cerr << "\n";
+//     llvm::errs() << "Constructing expression ";
+//     ExprPPrinter::printSingleExpr(llvm::errs(), e);
+//     llvm::errs() << "\n";
 
     switch (e->getKind()) {
 
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index f2e38182..d5598d1d 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -18,9 +18,10 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver,
                                        std::string path,
                                        const std::string& commentSign,
                                        int queryTimeToLog)                                  
-    : solver(_solver), 
-      os(path.c_str(), std::ios::trunc),
-      logBuffer(""),
+    : solver(_solver),
+      os(path.c_str(), ErrorInfo),
+      BufferString(""),
+      logBuffer(BufferString),
       queryCount(0),    
       minQueryTimeToLog(queryTimeToLog),
       startTime(0.0f),
@@ -79,8 +80,7 @@ void QueryLoggingSolver::flushBuffer() {
       }
       
       // prepare the buffer for reuse
-      logBuffer.clear();
-      logBuffer.str("");
+      BufferString = "";
 }
 
 bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 2c7d80e8..ad1722ca 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+#include "llvm/Support/raw_ostream.h"
 #include <fstream>
 #include <sstream>
 
@@ -25,9 +26,12 @@ class QueryLoggingSolver : public SolverImpl {
 
 protected:
     Solver *solver;
-    std::ofstream os;
-    std::ostringstream logBuffer; // buffer to store logs before flushing to 
-                                  // file
+    std::string ErrorInfo;
+    llvm::raw_fd_ostream os;
+    // @brief Buffer used by logBuffer
+    std::string BufferString;
+    // @brief buffer to store logs before flushing to file
+    llvm::raw_string_ostream logBuffer;
     unsigned queryCount;
     int minQueryTimeToLog; // we log to file only those queries
                            // which take longer than the specified time (ms);
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index e4a21f74..34ce0ede 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -34,7 +34,6 @@
 
 #include <algorithm> // max, min
 #include <cassert>
-#include <iostream>
 #include <map>
 #include <sstream>
 #include <vector>
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 025c70f2..229fa234 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -771,7 +771,6 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc,
     }
   }
 }
-#include <iostream>
 bool
 STPSolverImpl::computeInitialValues(const Query &query,
                                     const std::vector<const Array*> 
diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp
index 0e8b86dd..0d5e4568 100644
--- a/lib/Support/TreeStream.cpp
+++ b/lib/Support/TreeStream.cpp
@@ -10,12 +10,13 @@
 #include "klee/Internal/ADT/TreeStream.h"
 
 #include <cassert>
-#include <iostream>
 #include <iomanip>
 #include <fstream>
 #include <iterator>
 #include <map>
 
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/raw_ostream.h"
 #include <string.h>
 
 using namespace klee;
@@ -105,10 +106,9 @@ void TreeStreamWriter::readStream(TreeStreamID streamID,
   std::ifstream is(path.c_str(),
                    std::ios::in | std::ios::binary);
   assert(is.good());
-#if 0
-  std::cout << "finding chain for: " << streamID << "\n";
-#endif
-  
+  DEBUG_WITH_TYPE("TreeStreamWriter",
+                  llvm::errs() << "finding chain for: " << streamID << "\n");
+
   std::map<unsigned,unsigned> parents;
   std::vector<unsigned> roots;
   for (;;) {
@@ -137,11 +137,11 @@ void TreeStreamWriter::readStream(TreeStreamID streamID,
       while (size--) is.get();
     }
   }
-#if 0
-  std::cout << "roots: ";
-  std::copy(roots.begin(), roots.end(), std::ostream_iterator<unsigned>(std::cout, " "));
-  std::cout << "\n"; 
-#endif
+  DEBUG(llvm::errs() << "roots: ";
+	for (size_t i = 0, e = roots.size(); i < e; ++i) {
+	  llvm::errs() << roots[i] << " ";
+	}
+        llvm::errs() << "\n";);
   is.seekg(0, std::ios::beg);
   for (;;) {
     unsigned id;
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index abc37d4b..b19e2ea6 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -1,5 +1,3 @@
-#include <iostream>
-
 #include "expr/Lexer.h"
 #include "expr/Parser.h"
 
@@ -124,9 +122,11 @@ static std::string getQueryLogPath(const char filename[])
 	struct stat s;
 	if( !(stat(directoryToWriteQueryLogs.c_str(),&s) == 0 && S_ISDIR(s.st_mode)) )
 	{
-		std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" does not exist!" << std::endl;
-		exit(1);
-	}
+          llvm::errs() << "Directory to log queries \""
+                       << directoryToWriteQueryLogs << "\" does not exist!"
+                       << "\n";
+          exit(1);
+        }
 
 	//check permissions okay
 	if( !( (s.st_mode & S_IWUSR) && getuid() == s.st_uid) &&
@@ -134,9 +134,11 @@ static std::string getQueryLogPath(const char filename[])
 	    !( s.st_mode & S_IWOTH)
 	)
 	{
-		std::cerr << "Directory to log queries \"" << directoryToWriteQueryLogs << "\" is not writable!" << std::endl;
-		exit(1);
-	}
+          llvm::errs() << "Directory to log queries \""
+                       << directoryToWriteQueryLogs << "\" is not writable!"
+                       << "\n";
+          exit(1);
+        }
 
 	std::string path=directoryToWriteQueryLogs;
 	path+="/";
@@ -167,10 +169,9 @@ static void PrintInputTokens(const MemoryBuffer *MB) {
   Token T;
   do {
     L.Lex(T);
-    std::cout << "(Token \"" << T.getKindName() << "\" "
-               << "\"" << escapedString(T.start, T.length) << "\" "
-               << T.length << " "
-               << T.line << " " << T.column << ")\n";
+    llvm::outs() << "(Token \"" << T.getKindName() << "\" "
+                 << "\"" << escapedString(T.start, T.length) << "\" "
+                 << T.length << " " << T.line << " " << T.column << ")\n";
   } while (T.kind != Token::EndOfFile);
 }
 
@@ -185,7 +186,7 @@ static bool PrintInputAST(const char *Filename,
   while (Decl *D = P->ParseTopLevelDecl()) {
     if (!P->GetNumErrors()) {
       if (isa<QueryCommand>(D))
-        std::cout << "# Query " << ++NumQueries << "\n";
+        llvm::outs() << "# Query " << ++NumQueries << "\n";
 
       D->dump();
     }
@@ -194,8 +195,7 @@ static bool PrintInputAST(const char *Filename,
 
   bool success = true;
   if (unsigned N = P->GetNumErrors()) {
-    std::cerr << Filename << ": parse failure: "
-               << N << " errors.\n";
+    llvm::errs() << Filename << ": parse failure: " << N << " errors.\n";
     success = false;
   }
 
@@ -220,8 +220,7 @@ static bool EvaluateInputAST(const char *Filename,
 
   bool success = true;
   if (unsigned N = P->GetNumErrors()) {
-    std::cerr << Filename << ": parse failure: "
-               << N << " errors.\n";
+    llvm::errs() << Filename << ": parse failure: " << N << " errors.\n";
     success = false;
   }  
 
@@ -253,7 +252,7 @@ static bool EvaluateInputAST(const char *Filename,
               assert(false);
               break;
     };
-    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
   }
   else {
     coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
@@ -280,16 +279,16 @@ static bool EvaluateInputAST(const char *Filename,
          ie = Decls.end(); it != ie; ++it) {
     Decl *D = *it;
     if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
-      std::cout << "Query " << Index << ":\t";
+      llvm::outs() << "Query " << Index << ":\t";
 
       assert("FIXME: Support counterexample query commands!");
       if (QC->Values.empty() && QC->Objects.empty()) {
         bool result;
         if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
                           result)) {
-          std::cout << (result ? "VALID" : "INVALID");
+          llvm::outs() << (result ? "VALID" : "INVALID");
         } else {
-          std::cout << "FAIL (reason: " 
+          llvm::outs() << "FAIL (reason: "
                     << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
                     << ")";
         }
@@ -304,10 +303,10 @@ static bool EvaluateInputAST(const char *Filename,
         if (S->getValue(Query(ConstraintManager(QC->Constraints), 
                               QC->Values[0]),
                         result)) {
-          std::cout << "INVALID\n";
-          std::cout << "\tExpr 0:\t" << result;
+          llvm::outs() << "INVALID\n";
+          llvm::outs() << "\tExpr 0:\t" << result;
         } else {
-          std::cout << "FAIL (reason: " 
+          llvm::outs() << "FAIL (reason: "
                     << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode())
                     << ")";
         }
@@ -317,35 +316,35 @@ static bool EvaluateInputAST(const char *Filename,
         if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), 
                                       QC->Query),
                                 QC->Objects, result)) {
-          std::cout << "INVALID\n";
+          llvm::outs() << "INVALID\n";
 
           for (unsigned i = 0, e = result.size(); i != e; ++i) {
-            std::cout << "\tArray " << i << ":\t"
+            llvm::outs() << "\tArray " << i << ":\t"
                        << QC->Objects[i]->name
                        << "[";
             for (unsigned j = 0; j != QC->Objects[i]->size; ++j) {
-              std::cout << (unsigned) result[i][j];
+              llvm::outs() << (unsigned) result[i][j];
               if (j + 1 != QC->Objects[i]->size)
-                std::cout << ", ";
+                llvm::outs() << ", ";
             }
-            std::cout << "]";
+            llvm::outs() << "]";
             if (i + 1 != e)
-              std::cout << "\n";
+              llvm::outs() << "\n";
           }
         } else {
           SolverImpl::SolverRunStatus retCode = S->impl->getOperationStatusCode();
           if (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT == retCode) {
-            std::cout << " FAIL (reason: " 
+            llvm::outs() << " FAIL (reason: "
                       << SolverImpl::getOperationStatusString(retCode)
                       << ")";
           }           
           else {
-            std::cout << "VALID (counterexample request ignored)";
+            llvm::outs() << "VALID (counterexample request ignored)";
           }
         }
       }
 
-      std::cout << "\n";
+      llvm::outs() << "\n";
       ++Index;
     }
   }
@@ -358,7 +357,7 @@ static bool EvaluateInputAST(const char *Filename,
   delete S;
 
   if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) {
-    std::cout 
+    llvm::outs()
       << "--\n"
       << "total queries = " << queries << "\n"
       << "total queries constructs = " 
@@ -390,7 +389,7 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 	bool success = true;
 	if (unsigned N = P->GetNumErrors())
 	{
-		std::cerr << Filename << ": parse failure: "
+		llvm::errs() << Filename << ": parse failure: "
 				   << N << " errors.\n";
 		success = false;
 	}
@@ -399,7 +398,7 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 	return false;
 
 	ExprSMTLIBPrinter* printer = createSMTLIBPrinter();
-	printer->setOutput(std::cout);
+	printer->setOutput(llvm::outs());
 
 	unsigned int queryNumber = 0;
 	//Loop over the declarations
@@ -409,10 +408,10 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 		if (QueryCommand *QC = dyn_cast<QueryCommand>(D))
 		{
 			//print line break to separate from previous query
-			if(queryNumber!=0) 	std::cout << std::endl;
+			if(queryNumber!=0) 	llvm::outs() << "\n";
 
 			//Output header for this query as a SMT-LIBv2 comment
-			std::cout << ";SMTLIBv2 Query " << queryNumber << std::endl;
+			llvm::outs() << ";SMTLIBv2 Query " << queryNumber << "\n";
 
 			/* Can't pass ConstraintManager constructor directly
 			 * as argument to Query object. Like...
@@ -458,7 +457,7 @@ int main(int argc, char **argv) {
   OwningPtr<MemoryBuffer> MB;
   error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB);
   if (ec) {
-    std::cerr << argv[0] << ": error: " << ec.message() << "\n";
+    llvm::errs() << argv[0] << ": error: " << ec.message() << "\n";
     return 1;
   }
   
@@ -494,7 +493,7 @@ int main(int argc, char **argv) {
     success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder);
     break;
   default:
-    std::cerr << argv[0] << ": error: Unknown program action!\n";
+    llvm::errs() << argv[0] << ": error: Unknown program action!\n";
   }
 
   delete Builder;
diff --git a/tools/klee/Debug.cpp b/tools/klee/Debug.cpp
index 3d46de03..fbabed9d 100644
--- a/tools/klee/Debug.cpp
+++ b/tools/klee/Debug.cpp
@@ -1,12 +1,11 @@
 #include <klee/Expr.h>
-#include <iostream>
 
 void kdb_printExpr(klee::Expr *e) {
-  std::cerr << "expr: " << e << " -- ";
+  llvm::errs() << "expr: " << e << " -- ";
   if (e) {
-    std::cerr << *e;
+    llvm::errs() << *e;
   } else {
-    std::cerr << "(null)";
+    llvm::errs() << "(null)";
   }
-  std::cerr << "\n";
+  llvm::errs() << "\n";
 }
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 07c33f2a..0292376c 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -62,7 +62,6 @@
 #include <cerrno>
 #include <fstream>
 #include <iomanip>
-#include <iostream>
 #include <iterator>
 #include <sstream>
 
@@ -221,7 +220,7 @@ class KleeHandler : public InterpreterHandler {
 private:
   Interpreter *m_interpreter;
   TreeStreamWriter *m_pathWriter, *m_symPathWriter;
-  std::ostream *m_infoFile;
+  llvm::raw_ostream *m_infoFile;
 
   SmallString<128> m_outputDirectory;
 
@@ -236,7 +235,7 @@ public:
   KleeHandler(int argc, char **argv);
   ~KleeHandler();
 
-  std::ostream &getInfoStream() const { return *m_infoFile; }
+  llvm::raw_ostream &getInfoStream() const { return *m_infoFile; }
   unsigned getNumTestCases() { return m_testIndex; }
   unsigned getNumPathsExplored() { return m_pathsExplored; }
   void incPathsExplored() { m_pathsExplored++; }
@@ -248,9 +247,9 @@ public:
                        const char *errorSuffix);
 
   std::string getOutputFilename(const std::string &filename);
-  std::ostream *openOutputFile(const std::string &filename);
+  llvm::raw_fd_ostream *openOutputFile(const std::string &filename);
   std::string getTestFilename(const std::string &suffix, unsigned id);
-  std::ostream *openTestFile(const std::string &suffix, unsigned id);
+  llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id);
 
   // load a .out file
   static void loadOutFile(std::string name, 
@@ -370,16 +369,20 @@ std::string KleeHandler::getOutputFilename(const std::string &filename) {
   return path.str();
 }
 
-std::ostream *KleeHandler::openOutputFile(const std::string &filename) {
-  std::ios::openmode io_mode = std::ios::out | std::ios::trunc 
-                             | std::ios::binary;
-  std::ostream *f;
+llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) {
+  llvm::raw_fd_ostream *f;
+  std::string Error;
   std::string path = getOutputFilename(filename);
-  f = new std::ofstream(path.c_str(), io_mode);
-  if (!f) {
-    klee_error("error opening file \"%s\" (out of memory)", filename.c_str());
-  } else if (!f->good()) {
-    klee_error("error opening file \"%s\".  KLEE may have run out of file descriptors: try to increase the maximum number of open file descriptors by using ulimit.", filename.c_str());
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3,0)
+  f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_Binary);
+#else
+  f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary);
+#endif
+  if (!Error.empty()) {
+    klee_error("error opening file \"%s\".  KLEE may have run out of file "
+               "descriptors: try to increase the maximum number of open file "
+               "descriptors by using ulimit (%s).",
+               filename.c_str(), Error.c_str());
     delete f;
     f = NULL;
   }
@@ -393,7 +396,8 @@ std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id)
   return filename.str();
 }
 
-std::ostream *KleeHandler::openTestFile(const std::string &suffix, unsigned id) {
+llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix,
+                                                unsigned id) {
   return openOutputFile(getTestFilename(suffix, id));
 }
 
@@ -403,7 +407,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
                                   const char *errorMessage, 
                                   const char *errorSuffix) {
   if (errorMessage && ExitOnError) {
-    std::cerr << "EXITING ON ERROR:\n" << errorMessage << "\n";
+    llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n";
     exit(1);
   }
 
@@ -446,7 +450,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     }
 
     if (errorMessage) {
-      std::ostream *f = openTestFile(errorSuffix, id);
+      llvm::raw_ostream *f = openTestFile(errorSuffix, id);
       *f << errorMessage;
       delete f;
     }
@@ -455,16 +459,19 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       std::vector<unsigned char> concreteBranches;
       m_pathWriter->readStream(m_interpreter->getPathStreamID(state),
                                concreteBranches);
-      std::ostream *f = openTestFile("path", id);
-      std::copy(concreteBranches.begin(), concreteBranches.end(), 
-                std::ostream_iterator<unsigned char>(*f, "\n"));
+      llvm::raw_fd_ostream *f = openTestFile("path", id);
+      for (std::vector<unsigned char>::iterator I = concreteBranches.begin(),
+                                                E = concreteBranches.end();
+           I != E; ++I) {
+        *f << *I << "\n";
+      }
       delete f;
     }
    
     if (errorMessage || WritePCs) {
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
-      std::ostream *f = openTestFile("pc", id);
+      llvm::raw_ostream *f = openTestFile("pc", id);
       *f << constraints;
       delete f;
     }
@@ -472,7 +479,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     if (WriteCVCs) {
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
-      std::ostream *f = openTestFile("cvc", id);
+      llvm::raw_ostream *f = openTestFile("cvc", id);
       *f << constraints;
       delete f;
     }
@@ -480,7 +487,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     if(WriteSMT2s) {
     	std::string constraints;
         m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
-        std::ostream *f = openTestFile("smt2", id);
+        llvm::raw_ostream *f = openTestFile("smt2", id);
         *f << constraints;
         delete f;
     }
@@ -489,16 +496,17 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       std::vector<unsigned char> symbolicBranches;
       m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state),
                                   symbolicBranches);
-      std::ostream *f = openTestFile("sym.path", id);
-      std::copy(symbolicBranches.begin(), symbolicBranches.end(), 
-                std::ostream_iterator<unsigned char>(*f, "\n"));
+      llvm::raw_fd_ostream *f = openTestFile("sym.path", id);
+      for (std::vector<unsigned char>::iterator I = symbolicBranches.begin(), E = symbolicBranches.end(); I!=E; ++I) {
+        *f << *I << "\n";
+      }
       delete f;
     }
 
     if (WriteCov) {
       std::map<const std::string*, std::set<unsigned> > cov;
       m_interpreter->getCoveredLines(state, cov);
-      std::ostream *f = openTestFile("cov", id);
+      llvm::raw_ostream *f = openTestFile("cov", id);
       for (std::map<const std::string*, std::set<unsigned> >::iterator
              it = cov.begin(), ie = cov.end();
            it != ie; ++it) {
@@ -515,7 +523,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 
     if (WriteTestInfo) {
       double elapsed_time = util::getWallTime() - start_time;
-      std::ostream *f = openTestFile("info", id);
+      llvm::raw_ostream *f = openTestFile("info", id);
       *f << "Time to generate test case: " 
          << elapsed_time << "s\n";
       delete f;
@@ -550,8 +558,8 @@ void KleeHandler::getOutFiles(std::string path,
   }
 
   if (ec) {
-    std::cerr << "ERROR: unable to read output directory: " << path
-               << ": " << ec.message() << "\n";
+    llvm::errs() << "ERROR: unable to read output directory: " << path << ": "
+                 << ec.message() << "\n";
     exit(1);
   }
 }
@@ -954,11 +962,11 @@ void stop_forking() {
 
 static void interrupt_handle() {
   if (!interrupted && theInterpreter) {
-    std::cerr << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
+    llvm::errs() << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
     halt_execution();
     sys::SetInterruptFunction(interrupt_handle);
   } else {
-    std::cerr << "KLEE: ctrl-c detected, exiting.\n";
+    llvm::errs() << "KLEE: ctrl-c detected, exiting.\n";
     exit(1);
   }
   interrupted = true;
@@ -1292,7 +1300,7 @@ int main(int argc, char **argv, char **envp) {
   // locale and other data and then calls main.
   Function *mainFn = mainModule->getFunction("main");
   if (!mainFn) {
-    std::cerr << "'main' function not found in module.\n";
+    llvm::errs() << "'main' function not found in module.\n";
     return -1;
   }
 
@@ -1347,8 +1355,8 @@ int main(int argc, char **argv, char **envp) {
   Interpreter *interpreter = 
     theInterpreter = Interpreter::create(IOpts, handler);
   handler->setInterpreter(interpreter);
-  
-  std::ostream &infoFile = handler->getInfoStream();
+
+  llvm::raw_ostream &infoFile = handler->getInfoStream();
   for (int i=0; i<argc; i++) {
     infoFile << argv[i] << (i+1<argc ? " ":"\n");
   }
@@ -1386,7 +1394,7 @@ int main(int argc, char **argv, char **envp) {
       if (out) {
         kTests.push_back(out);
       } else {
-        std::cerr << "KLEE: unable to open: " << *it << "\n";
+        llvm::errs() << "KLEE: unable to open: " << *it << "\n";
       }
     }
 
@@ -1403,8 +1411,9 @@ int main(int argc, char **argv, char **envp) {
          it != ie; ++it) {
       KTest *out = *it;
       interpreter->setReplayOut(out);
-      std::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)"
-                 << " (" << ++i << "/" << outFiles.size() << ")\n";
+      llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out)
+                   << " bytes)"
+                   << " (" << ++i << "/" << outFiles.size() << ")\n";
       // XXX should put envp in .ktest ?
       interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
       if (interrupted) break;
@@ -1421,7 +1430,7 @@ int main(int argc, char **argv, char **envp) {
          it != ie; ++it) {
       KTest *out = kTest_fromFile(it->c_str());
       if (!out) {
-        std::cerr << "KLEE: unable to open: " << *it << "\n";
+        llvm::errs() << "KLEE: unable to open: " << *it << "\n";
         exit(1);
       }
       seeds.push_back(out);
@@ -1436,19 +1445,19 @@ int main(int argc, char **argv, char **envp) {
            it2 != ie; ++it2) {
         KTest *out = kTest_fromFile(it2->c_str());
         if (!out) {
-          std::cerr << "KLEE: unable to open: " << *it2 << "\n";
+          llvm::errs() << "KLEE: unable to open: " << *it2 << "\n";
           exit(1);
         }
         seeds.push_back(out);
       }
       if (outFiles.empty()) {
-        std::cerr << "KLEE: seeds directory is empty: " << *it << "\n";
+        llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n";
         exit(1);
       }
     }
        
     if (!seeds.empty()) {
-      std::cerr << "KLEE: using " << seeds.size() << " seeds\n";
+      llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n";
       interpreter->useSeeds(&seeds);
     }
     if (RunInDir != "") {
@@ -1518,7 +1527,7 @@ int main(int argc, char **argv, char **envp) {
         << handler->getNumPathsExplored() << "\n";
   stats << "KLEE: done: generated tests = " 
         << handler->getNumTestCases() << "\n";
-  std::cerr << stats.str();
+  llvm::errs() << stats.str();
   handler->getInfoStream() << stats.str();
 
   BufferPtr.take();
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index f1cd4ec4..a9bfeda1 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -9,4 +9,5 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
+CXXFLAGS += -DLLVM_29_UNITTEST
 LIBS += -lstp