about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Basic/ConstructSolverChain.cpp18
-rw-r--r--lib/Basic/Makefile1
-rw-r--r--lib/Core/ExecutionState.cpp66
-rw-r--r--lib/Core/Executor.cpp184
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/ExecutorTimers.cpp6
-rw-r--r--lib/Core/ExecutorUtil.cpp3
-rw-r--r--lib/Core/ExternalDispatcher.cpp3
-rw-r--r--lib/Core/ImpliedValue.cpp3
-rwxr-xr-xlib/Core/Makefile1
-rw-r--r--lib/Core/Memory.cpp19
-rw-r--r--lib/Core/PTree.cpp3
-rw-r--r--lib/Core/PTree.h6
-rw-r--r--lib/Core/Searcher.cpp29
-rw-r--r--lib/Core/Searcher.h30
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp73
-rw-r--r--lib/Core/SpecialFunctionHandler.h33
-rw-r--r--lib/Core/StatsTracker.cpp39
-rw-r--r--lib/Core/StatsTracker.h4
-rw-r--r--lib/Core/UserSearcher.cpp14
-rw-r--r--lib/Expr/Constraints.cpp1
-rw-r--r--lib/Expr/Expr.cpp12
-rw-r--r--lib/Expr/ExprPPrinter.cpp26
-rw-r--r--lib/Expr/ExprSMTLIBLetPrinter.cpp445
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp1725
-rw-r--r--lib/Expr/Lexer.cpp1
-rw-r--r--lib/Expr/Makefile1
-rw-r--r--lib/Expr/Parser.cpp27
-rw-r--r--lib/Expr/Updates.cpp10
-rw-r--r--lib/Module/Checks.cpp11
-rw-r--r--lib/Module/InstructionInfoTable.cpp88
-rw-r--r--lib/Module/KModule.cpp87
-rwxr-xr-xlib/Module/Makefile1
-rw-r--r--lib/Module/ModuleUtil.cpp368
-rw-r--r--lib/Module/Optimize.cpp5
-rw-r--r--lib/SMT/SMTParser.cpp11
-rw-r--r--lib/SMT/SMTParser.h2
-rw-r--r--lib/SMT/main.cpp3
-rw-r--r--lib/SMT/smtlib.y2
-rw-r--r--lib/Solver/FastCexSolver.cpp64
-rw-r--r--lib/Solver/IndependentSolver.cpp39
-rwxr-xr-xlib/Solver/Makefile3
-rw-r--r--lib/Solver/MetaSMTBuilder.h18
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp10
-rw-r--r--lib/Solver/QueryLoggingSolver.h10
-rw-r--r--lib/Solver/STPBuilder.cpp108
-rw-r--r--lib/Solver/STPBuilder.h19
-rw-r--r--lib/Solver/Solver.cpp17
-rw-r--r--lib/Support/Makefile1
-rw-r--r--lib/Support/MemoryUsage.cpp25
-rw-r--r--lib/Support/TreeStream.cpp20
51 files changed, 2062 insertions, 1638 deletions
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/Basic/Makefile b/lib/Basic/Makefile
index d4481e7f..e72399a2 100644
--- a/lib/Basic/Makefile
+++ b/lib/Basic/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeBasic
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
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 ef55f21f..f31d6aeb 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -47,6 +47,7 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Support/FloatEvaluation.h"
 #include "klee/Internal/System/Time.h"
+#include "klee/Internal/System/MemoryUsage.h"
 
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Function.h"
@@ -85,8 +86,8 @@
 
 #include <cassert>
 #include <algorithm>
-#include <iostream>
 #include <iomanip>
+#include <iosfwd>
 #include <fstream>
 #include <sstream>
 #include <vector>
@@ -163,6 +164,11 @@ namespace {
   SimplifySymIndices("simplify-sym-indices",
                      cl::init(false));
 
+  cl::opt<bool>
+  EqualitySubstitution("equality-substitution",
+                     cl::init(true),
+                     cl::desc("Simplify equality expressions before querying the solver (default=on)."));
+
   cl::opt<unsigned>
   MaxSymArraySize("max-sym-array-size",
                   cl::init(0));
@@ -315,7 +321,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);
@@ -332,7 +338,7 @@ Executor::Executor(const InterpreterOptions &opts,
                          interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
                          interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
   
-  this->solver = new TimingSolver(solver);
+  this->solver = new TimingSolver(solver, EqualitySubstitution);
 
   memory = new MemoryManager();
 }
@@ -1104,12 +1110,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
@@ -1166,7 +1173,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';
   }
 
@@ -1350,10 +1357,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
@@ -2584,11 +2591,7 @@ void Executor::run(ExecutionState &initialState) {
         // We need to avoid calling GetMallocUsage() often because it
         // is O(elts on freelist). This is really bad since we start
         // to pummel the freelist once we hit the memory cap.
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
-        unsigned mbs = sys::Process::GetMallocUsage() >> 20;
-#else
-        unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20;
-#endif
+        unsigned mbs = util::GetTotalMallocUsage() >> 20;
         if (mbs > MaxMemory) {
           if (mbs > MaxMemory + 100) {
             // just guess at how many to kill
@@ -2627,7 +2630,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) {
@@ -2641,7 +2644,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)) {
@@ -2729,29 +2733,74 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
   terminateState(state);
 }
 
+const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state,
+    Instruction ** lastInstruction) {
+  // unroll the stack of the applications state and find
+  // the last instruction which is not inside a KLEE internal function
+  ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(),
+      itE = state.stack.rend();
+
+  // don't check beyond the outermost function (i.e. main())
+  itE--;
+
+  const InstructionInfo * ii = 0;
+  if (kmodule->internalFunctions.count(it->kf->function) == 0){
+    ii =  state.prevPC->info;
+    *lastInstruction = state.prevPC->inst;
+    //  Cannot return yet because even though
+    //  it->function is not an internal function it might of
+    //  been called from an internal function.
+  }
+
+  // Wind up the stack and check if we are in a KLEE internal function.
+  // We visit the entire stack because we want to return a CallInstruction
+  // that was not reached via any KLEE internal functions.
+  for (;it != itE; ++it) {
+    // check calling instruction and if it is contained in a KLEE internal function
+    const Function * f = (*it->caller).inst->getParent()->getParent();
+    if (kmodule->internalFunctions.count(f)){
+      ii = 0;
+      continue;
+    }
+    if (!ii){
+      ii = (*it->caller).info;
+      *lastInstruction = (*it->caller).inst;
+    }
+  }
+
+  if (!ii) {
+    // something went wrong, play safe and return the current instruction info
+    *lastInstruction = state.prevPC->inst;
+    return *state.prevPC->info;
+  }
+  return *ii;
+}
 void Executor::terminateStateOnError(ExecutionState &state,
                                      const llvm::Twine &messaget,
                                      const char *suffix,
                                      const llvm::Twine &info) {
   std::string message = messaget.str();
   static std::set< std::pair<Instruction*, std::string> > emittedErrors;
-  const InstructionInfo &ii = *state.prevPC->info;
+  Instruction * lastInst;
+  const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst);
   
   if (EmitAllErrors ||
-      emittedErrors.insert(std::make_pair(state.prevPC->inst, message)).second) {
+      emittedErrors.insert(std::make_pair(lastInst, message)).second) {
     if (ii.file != "") {
       klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
     } else {
-      klee_message("ERROR: %s", message.c_str());
+      klee_message("ERROR: (location information missing) %s", message.c_str());
     }
     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";
       msg << "Line: " << ii.line << "\n";
+      msg << "assembly.ll line: " << ii.assemblyLine << "\n";
     }
     msg << "Stack: \n";
     state.dumpStack(msg);
@@ -2759,6 +2808,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);
   }
     
@@ -2783,8 +2833,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;
   }
@@ -2823,7 +2873,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];
@@ -2867,11 +2919,11 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   if (!n || replayOut || replayPath)
     return e;
 
-  // right now, we don't replace symbolics (is there any reason too?)
+  // right now, we don't replace symbolics (is there any reason to?)
   if (!isa<ConstantExpr>(e))
     return e;
 
-  if (n != 1 && random() %  n)
+  if (n != 1 && random() % n)
     return e;
 
   // create a new fresh location, assert it is equal to concrete value in e
@@ -2882,7 +2934,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;
 }
@@ -2994,7 +3046,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";
@@ -3392,48 +3446,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,
@@ -3468,8 +3515,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/Executor.h b/lib/Core/Executor.h
index b7318a2c..7d82332c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -340,6 +340,11 @@ private:
   /// Get textual information regarding a memory address.
   std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const;
 
+  // Determines the \param lastInstruction of the \param state which is not KLEE
+  // internal and returns its InstructionInfo
+  const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state,
+      llvm::Instruction** lastInstruction);
+
   // remove state from queue and delete
   void terminateState(ExecutionState &state);
   // call exit handler and terminate state
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/Makefile b/lib/Core/Makefile
index 4da3c7ea..f34f699d 100755
--- a/lib/Core/Makefile
+++ b/lib/Core/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeCore
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
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 2dbabd01..2610f17e 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -157,10 +157,8 @@ void RandomSearcher::update(ExecutionState *current,
 
 ///
 
-WeightedRandomSearcher::WeightedRandomSearcher(Executor &_executor,
-                                               WeightType _type) 
-  : executor(_executor),
-    states(new DiscretePDF<ExecutionState*>()),
+WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
+  : states(new DiscretePDF<ExecutionState*>()),
     type(_type) {
   switch(type) {
   case Depth: 
@@ -413,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
@@ -442,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) {
@@ -466,7 +464,7 @@ ExecutionState &MergingSearcher::selectState() {
   }
   
   if (DebugLogMerge)
-    std::cerr << "-- merge complete, continuing --\n";
+    llvm::errs() << "-- merge complete, continuing --\n";
   
   return selectState();
 }
@@ -514,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;
       }
     }
@@ -580,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 79c233c4..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";
     }
   };
@@ -135,7 +134,6 @@ namespace klee {
     };
 
   private:
-    Executor &executor;
     DiscretePDF<ExecutionState*> *states;
     WeightType type;
     bool updateWeights;
@@ -143,7 +141,7 @@ namespace klee {
     double getWeight(ExecutionState*);
 
   public:
-    WeightedRandomSearcher(Executor &executor, WeightType type);
+    WeightedRandomSearcher(WeightType type);
     ~WeightedRandomSearcher();
 
     ExecutionState &selectState();
@@ -151,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;
@@ -177,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";
     }
   };
@@ -200,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";
     }
   };
@@ -223,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";
     }
   };
@@ -248,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";
@@ -271,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";
     }
   };
@@ -291,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 04f32780..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>
 
@@ -38,20 +39,14 @@ using namespace klee;
 
 ///
 
-struct HandlerInfo {
-  const char *name;
-  SpecialFunctionHandler::Handler handler;
-  bool doesNotReturn; /// Intrinsic terminates the process
-  bool hasReturnValue; /// Intrinsic has a return value
-  bool doNotOverride; /// Intrinsic should not be used if already defined
-};
+
 
 // FIXME: We are more or less committed to requiring an intrinsic
 // library these days. We can move some of this stuff there,
 // especially things like realloc which have complicated semantics
 // w.r.t. forking. Among other things this makes delayed query
 // dispatch easier to implement.
-HandlerInfo handlerInfo[] = {
+static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
 #define add(name, handler, ret) { name, \
                                   &SpecialFunctionHandler::handler, \
                                   false, ret, false }
@@ -117,12 +112,37 @@ HandlerInfo handlerInfo[] = {
 #undef add  
 };
 
+SpecialFunctionHandler::const_iterator SpecialFunctionHandler::begin() {
+  return SpecialFunctionHandler::const_iterator(handlerInfo);
+}
+
+SpecialFunctionHandler::const_iterator SpecialFunctionHandler::end() {
+  // NULL pointer is sentinel
+  return SpecialFunctionHandler::const_iterator(0);
+}
+
+SpecialFunctionHandler::const_iterator& SpecialFunctionHandler::const_iterator::operator++() {
+  ++index;
+  if ( index >= SpecialFunctionHandler::size())
+  {
+    // Out of range, return .end()
+    base=0; // Sentinel
+    index=0;
+  }
+
+  return *this;
+}
+
+int SpecialFunctionHandler::size() {
+	return sizeof(handlerInfo)/sizeof(handlerInfo[0]);
+}
+
 SpecialFunctionHandler::SpecialFunctionHandler(Executor &_executor) 
   : executor(_executor) {}
 
 
 void SpecialFunctionHandler::prepare() {
-  unsigned N = sizeof(handlerInfo)/sizeof(handlerInfo[0]);
+  unsigned N = size();
 
   for (unsigned i=0; i<N; ++i) {
     HandlerInfo &hi = handlerInfo[i];
@@ -232,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");
@@ -260,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);
@@ -273,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, 
@@ -289,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, 
@@ -307,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, 
@@ -425,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,
@@ -447,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,
@@ -478,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;
@@ -490,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,
@@ -715,3 +736,5 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
+
+
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 02e70ed4..f68c6edb 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SPECIALFUNCTIONHANDLER_H
 #define KLEE_SPECIALFUNCTIONHANDLER_H
 
+#include <iterator>
 #include <map>
 #include <vector>
 #include <string>
@@ -37,6 +38,38 @@ namespace klee {
     handlers_ty handlers;
     class Executor &executor;
 
+    struct HandlerInfo {
+      const char *name;
+      SpecialFunctionHandler::Handler handler;
+      bool doesNotReturn; /// Intrinsic terminates the process
+      bool hasReturnValue; /// Intrinsic has a return value
+      bool doNotOverride; /// Intrinsic should not be used if already defined
+    };
+
+    // const_iterator to iterate over stored HandlerInfo
+    // FIXME: Implement >, >=, <=, < operators
+    class const_iterator : public std::iterator<std::random_access_iterator_tag, HandlerInfo>
+    {
+      private:
+        value_type* base;
+        int index;
+      public:
+      const_iterator(value_type* hi) : base(hi), index(0) {};
+      const_iterator& operator++();  // pre-fix
+      const_iterator operator++(int); // post-fix
+      const value_type& operator*() { return base[index];}
+      const value_type* operator->() { return &(base[index]);}
+      const value_type& operator[](int i) { return base[i];}
+      bool operator==(const_iterator& rhs) { return (rhs.base + rhs.index) == (this->base + this->index);}
+      bool operator!=(const_iterator& rhs) { return !(*this == rhs);}
+    };
+
+    static const_iterator begin();
+    static const_iterator end();
+    static int size();
+
+
+
   public:
     SpecialFunctionHandler(Executor &_executor);
 
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 8161a52c..0946d2ba 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -46,15 +46,12 @@
 #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"
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
 #include "llvm/Support/FileSystem.h"
-#endif
 
-#include <iostream>
 #include <fstream>
+#include <unistd.h>
 
 using namespace klee;
 using namespace llvm;
@@ -182,20 +179,15 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
     updateMinDistToUncovered(_updateMinDistToUncovered) {
   KModule *km = executor.kmodule;
 
-  sys::Path module(objectFilename);
-#if LLVM_VERSION_CODE < LLVM_VERSION(3, 1)
-  if (!sys::Path(objectFilename).isAbsolute()) {
-#else
   if (!sys::path::is_absolute(objectFilename)) {
-#endif
-    sys::Path current = sys::Path::GetCurrentDirectory();
-    current.appendComponent(objectFilename);
-#if LLVM_VERSION_CODE < LLVM_VERSION(3, 1)
-    if (current.exists())
-#else
-    if (sys::fs::exists(current.c_str()))
-#endif
-      objectFilename = current.c_str();
+    SmallString<128> current(objectFilename);
+    if(sys::fs::make_absolute(current)) {
+      bool exists = false;
+      error_code ec = sys::fs::exists(current.str(), exists);
+      if (ec == errc::success && exists) {
+        objectFilename = current.c_str();
+      }
+    }
   }
 
   if (OutputIStats)
@@ -438,15 +430,16 @@ 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";
-  of << "pid: " << sys::Process::GetCurrentUserId() << "\n";
+  of << "pid: " << getpid() << "\n";
   of << "cmd: " << m->getModuleIdentifier() << "\n\n";
   of << "\n";
   
@@ -570,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 a20ae968..72f3351f 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -81,12 +81,12 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
   case Searcher::BFS: searcher = new BFSSearcher(); break;
   case Searcher::RandomState: searcher = new RandomSearcher(); break;
   case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
-  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
-  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::MinDistToUncovered); break;
-  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::Depth); break;
-  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::InstCount); break;
-  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CPInstCount); break;
-  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::QueryCost); break;
+  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew); break;
+  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered); break;
+  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth); break;
+  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount); break;
+  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount); break;
+  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost); break;
   }
 
   return searcher;
@@ -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 ac1d1d01..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,10 +45,11 @@ 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;
+  bool forceNoLineBreaks;
   std::string newline;
 
   /// shouldPrintWidth - Predicate for whether this expression should
@@ -299,7 +298,7 @@ private:
   }
 
 public:
-  PPrinter(std::ostream &_os) : os(_os), newline("\n") {
+  PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") {
     reset();
   }
 
@@ -307,10 +306,15 @@ public:
     newline = _newline;
   }
 
+  void setForceNoLineBreaks(bool _forceNoLineBreaks) {
+    forceNoLineBreaks = _forceNoLineBreaks;
+  }
+
   void reset() {
     counter = 0;
     updateCounter = 0;
     hasScan = false;
+    forceNoLineBreaks = false;
     bindings.clear();
     updateBindings.clear();
     couldPrint.clear();
@@ -412,7 +416,7 @@ public:
   /* Public utility functions */
 
   void printSeparator(PrintContext &PC, bool simple, unsigned indent) {
-    if (simple) {
+    if (simple || forceNoLineBreaks) {
       PC << ' ';
     } else {
       PC.breakLine(indent);
@@ -420,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);
@@ -438,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);
 
@@ -448,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 7225704e..d4243452 100644
--- a/lib/Expr/ExprSMTLIBLetPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -1,4 +1,5 @@
-//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*-
+//C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,243 +8,225 @@
 //
 //===----------------------------------------------------------------------===//
 
-#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",
+                  llvm::cl::desc("Enables generated SMT-LIBv2 files to use "
+                                 "(let) expressions (default=on)"),
+                  llvm::cl::init(true));
+}
+
+namespace klee {
+const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
 
-namespace ExprSMTLIBOptions
-{
-	llvm::cl::opt<bool> useLetExpressions("smtlib-use-let-expressions",
-			llvm::cl::desc("Enables generated SMT-LIBv2 files to use (let) expressions (default=on)"),
-			llvm::cl::init(true)
-	);
+ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter()
+    : bindings(), firstEO(), twoOrMoreEO(), disablePrintedAbbreviations(false) {
 }
 
-namespace klee
-{
-	const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
-
-
-	ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() :
-	bindings(), firstEO(), twoOrMoreEO(),
-	disablePrintedAbbreviations(false)
-	{
-	}
-
-	void ExprSMTLIBLetPrinter::generateOutput()
-	{
-		if(p==NULL || query == NULL || o ==NULL)
-		{
-			std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
-			return;
-		}
-
-		generateBindings();
-
-		if(isHumanReadable()) printNotice();
-		printOptions();
-		printSetLogic();
-		printArrayDeclarations();
-		printLetExpression();
-		printAction();
-		printExit();
-	}
-
-	void ExprSMTLIBLetPrinter::scan(const ref<Expr>& e)
-	{
-		if(isa<ConstantExpr>(e))
-			return; //we don't need to scan simple constants
-
-		if(firstEO.insert(e).second)
-		{
-			//We've not seen this expression before
-
-			if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
-			{
-
-				//Attempt to insert array and if array wasn't present before do more things
-				if(usedArrays.insert(re->updates.root).second)
-				{
-
-					//check if the array is constant
-					if( re->updates.root->isConstantArray())
-						haveConstantArray=true;
-
-					//scan the update list
-					scanUpdates(re->updates.head);
-
-				}
-
-			}
-
-			//recurse into the children
-			Expr* ep = e.get();
-			for(unsigned int i=0; i < ep->getNumKids(); i++)
-				scan(ep->getKid(i));
-		}
-		else
-		{
-			/* We must of seen the expression before. Add it to
-			 * the set of twoOrMoreOccurances. We don't need to
-			 * check if the insertion fails.
-			 */
-			twoOrMoreEO.insert(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();
-				i!= twoOrMoreEO.end(); ++i)
-		{
-			bindings.insert(std::make_pair(*i,counter));
-			++counter;
-		}
-	}
-
-	void ExprSMTLIBLetPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
-	{
-		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.
-			 * Do this by using the parent method.
-			 */
-			ExprSMTLIBPrinter::printExpression(e,expectedSort);
-		}
-		else
-		{
-			//Use binding name e.g. "?B1"
-
-			/* Handle the corner case where the expectedSort
-			 * doesn't match the sort of the abbreviation. Not really very efficient (calls bindings.find() twice),
-			 * we'll cast and call ourself again but with the correct expectedSort.
-			 */
-			if(getSort(e) != expectedSort)
-			{
-				printCastToSort(e,expectedSort);
-				return;
-			}
-
-			// No casting is needed in this depth of recursion, just print the abbreviation
-			*p << BINDING_PREFIX << i->second;
-		}
-	}
-
-	void ExprSMTLIBLetPrinter::reset()
-	{
-		//Let parent clean up first
-		ExprSMTLIBPrinter::reset();
-
-		firstEO.clear();
-		twoOrMoreEO.clear();
-		bindings.clear();
-	}
-
-	void ExprSMTLIBLetPrinter::printLetExpression()
-	{
-		*p << "(assert"; p->pushIndent(); printSeperator();
-
-		if(bindings.size() !=0 )
-		{
-			//Only print let expression if we have bindings to use.
-			*p << "(let"; p->pushIndent(); printSeperator();
-			*p << "( "; p->pushIndent();
-
-			//Print each binding
-			for(map<const ref<Expr>, unsigned int>::const_iterator i= bindings.begin();
-					i!=bindings.end(); ++i)
-			{
-				printSeperator();
-				*p << "(" << BINDING_PREFIX << i->second << " ";
-				p->pushIndent();
-
-				//Disable abbreviations so none are used here.
-				disablePrintedAbbreviations=true;
-
-				//We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
-				printExpression(i->first,getSort(i->first));
-
-				p->popIndent();
-				printSeperator();
-				*p << ")";
-			}
-
-
-			p->popIndent(); printSeperator();
-			*p << ")";
-			printSeperator();
-
-			//Re-enable printing abbreviations.
-			disablePrintedAbbreviations=false;
-
-		}
-
-		//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();
-
-		/* Produce nested (and () () statements. If the constraint set
-		 * is empty then we will only print the "queryAssert".
-		 */
-		for(; itemsLeft !=0; --itemsLeft)
-		{
-			if(itemsLeft >=2)
-			{
-				*p << "(and"; p->pushIndent(); printSeperator();
-				printExpression(*constraint,SORT_BOOL); //We must and together bool expressions
-				printSeperator();
-				++constraint;
-				continue;
-			}
-			else
-			{
-				// must have 1 item left (i.e. the "queryAssert")
-				if(isHumanReadable()) { *p << "; query"; p->breakLineI();}
-				printExpression(queryAssert,SORT_BOOL); //The query must be a bool expression
-
-			}
-		}
-
-		/* Produce closing brackets for nested "and statements".
-		 * Number of "nested ands" = numberOfItems -1
-		 */
-		itemsLeft= numberOfItems -1;
-		for(; itemsLeft!=0; --itemsLeft)
-		{
-			p->popIndent(); printSeperator();
-			*p << ")";
-		}
-
-
-
-		if(bindings.size() !=0)
-		{
-			//end let expression
-			p->popIndent(); printSeperator();
-			*p << ")";  printSeperator();
-		}
-
-		//end assert
-		p->popIndent(); printSeperator();
-		*p << ")";
-		p->breakLineI();
-	}
-
-	ExprSMTLIBPrinter* createSMTLIBPrinter()
-	{
-		if(ExprSMTLIBOptions::useLetExpressions)
-			return new ExprSMTLIBLetPrinter();
-		else
-			return new ExprSMTLIBPrinter();
-	}
+void ExprSMTLIBLetPrinter::generateOutput() {
+  if (p == NULL || query == NULL || o == NULL) {
+    llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n";
+    return;
+  }
+
+  generateBindings();
+
+  if (isHumanReadable())
+    printNotice();
+  printOptions();
+  printSetLogic();
+  printArrayDeclarations();
+  printLetExpression();
+  printAction();
+  printExit();
+}
 
+void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) {
+  if (isa<ConstantExpr>(e))
+    return; // we don't need to scan simple constants
+
+  if (firstEO.insert(e).second) {
+    // We've not seen this expression before
+
+    if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+
+      // Attempt to insert array and if array wasn't present before do more
+      // things
+      if (usedArrays.insert(re->updates.root).second) {
+
+        // check if the array is constant
+        if (re->updates.root->isConstantArray())
+          haveConstantArray = true;
+
+        // scan the update list
+        scanUpdates(re->updates.head);
+      }
+    }
+
+    // recurse into the children
+    Expr *ep = e.get();
+    for (unsigned int i = 0; i < ep->getNumKids(); i++)
+      scan(ep->getKid(i));
+  } else {
+    /* We must of seen the expression before. Add it to
+     * the set of twoOrMoreOccurances. We don't need to
+     * check if the insertion fails.
+     */
+    twoOrMoreEO.insert(e);
+  }
+}
 
+void ExprSMTLIBLetPrinter::generateBindings() {
+  // Assign a number to each binding that will be used
+  unsigned int counter = 0;
+  for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
+       i != twoOrMoreEO.end(); ++i) {
+    bindings.insert(std::make_pair(*i, counter));
+    ++counter;
+  }
 }
 
+void ExprSMTLIBLetPrinter::printExpression(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
+  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.
+     * Do this by using the parent method.
+     */
+    ExprSMTLIBPrinter::printExpression(e, expectedSort);
+  } else {
+    // Use binding name e.g. "?B1"
+
+    /* Handle the corner case where the expectedSort
+     * doesn't match the sort of the abbreviation. Not really very efficient
+     * (calls bindings.find() twice),
+     * we'll cast and call ourself again but with the correct expectedSort.
+     */
+    if (getSort(e) != expectedSort) {
+      printCastToSort(e, expectedSort);
+      return;
+    }
+
+    // No casting is needed in this depth of recursion, just print the
+    // abbreviation
+    *p << BINDING_PREFIX << i->second;
+  }
+}
+
+void ExprSMTLIBLetPrinter::reset() {
+  // Let parent clean up first
+  ExprSMTLIBPrinter::reset();
+
+  firstEO.clear();
+  twoOrMoreEO.clear();
+  bindings.clear();
+}
+
+void ExprSMTLIBLetPrinter::printLetExpression() {
+  *p << "(assert";
+  p->pushIndent();
+  printSeperator();
+
+  if (bindings.size() != 0) {
+    // Only print let expression if we have bindings to use.
+    *p << "(let";
+    p->pushIndent();
+    printSeperator();
+    *p << "( ";
+    p->pushIndent();
+
+    // Print each binding
+    for (std::map<const ref<Expr>, unsigned int>::const_iterator i =
+             bindings.begin();
+         i != bindings.end(); ++i) {
+      printSeperator();
+      *p << "(" << BINDING_PREFIX << i->second << " ";
+      p->pushIndent();
+
+      // Disable abbreviations so none are used here.
+      disablePrintedAbbreviations = true;
+
+      // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
+      printExpression(i->first, getSort(i->first));
+
+      p->popIndent();
+      printSeperator();
+      *p << ")";
+    }
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    printSeperator();
+
+    // Re-enable printing abbreviations.
+    disablePrintedAbbreviations = false;
+  }
+
+  // print out Expressions with abbreviations.
+  unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
+  unsigned int itemsLeft = numberOfItems;
+  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".
+   */
+  for (; itemsLeft != 0; --itemsLeft) {
+    if (itemsLeft >= 2) {
+      *p << "(and";
+      p->pushIndent();
+      printSeperator();
+      printExpression(*constraint,
+                      SORT_BOOL); // We must and together bool expressions
+      printSeperator();
+      ++constraint;
+      continue;
+    } else {
+      // must have 1 item left (i.e. the "queryAssert")
+      if (isHumanReadable()) {
+        *p << "; query";
+        p->breakLineI();
+      }
+      printExpression(queryAssert,
+                      SORT_BOOL); // The query must be a bool expression
+    }
+  }
+
+  /* Produce closing brackets for nested "and statements".
+   * Number of "nested ands" = numberOfItems -1
+   */
+  itemsLeft = numberOfItems - 1;
+  for (; itemsLeft != 0; --itemsLeft) {
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+  }
+
+  if (bindings.size() != 0) {
+    // end let expression
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    printSeperator();
+  }
+
+  // end assert
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+  p->breakLineI();
+}
+
+ExprSMTLIBPrinter *createSMTLIBPrinter() {
+  if (ExprSMTLIBOptions::useLetExpressions)
+    return new ExprSMTLIBLetPrinter();
+  else
+    return new ExprSMTLIBPrinter();
+}
+}
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 9e97a4e0..bbb82d0d 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -1,4 +1,4 @@
-//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -6,901 +6,896 @@
 // 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>
+argConstantDisplayMode(
+    "smtlib-display-constants",
+    llvm::cl::desc("Sets how bitvector constants are written in generated "
+                   "SMT-LIBv2 files (default=dec)"),
+    llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin",
+                                "Use binary form (e.g. #b00101101)"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex",
+                                "Use Hexadecimal form (e.g. #x2D)"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec",
+                                "Use decimal form (e.g. (_ bv45 8) )"),
+                     clEnumValEnd),
+    llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL));
+
+llvm::cl::opt<bool> humanReadableSMTLIB(
+    "smtlib-human-readable",
+    llvm::cl::desc(
+        "Enables generated SMT-LIBv2 files to be human readable (default=off)"),
+    llvm::cl::init(false));
+}
+
+namespace klee {
+
+ExprSMTLIBPrinter::ExprSMTLIBPrinter()
+    : usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false),
+      logicToUse(QF_AUFBV),
+      humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB),
+      smtlibBoolOptions(), arraysToCallGetValueOn(NULL) {
+  setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
+}
+
+ExprSMTLIBPrinter::~ExprSMTLIBPrinter() {
+  if (p != NULL)
+    delete p;
+}
+
+void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) {
+  o = &output;
+  if (p != NULL)
+    delete p;
+
+  p = new PrintContext(output);
+}
+
+void ExprSMTLIBPrinter::setQuery(const Query &q) {
+  query = &q;
+  reset(); // clear the data structures
+  scanAll();
+  negateQueryExpression();
+}
+
+void ExprSMTLIBPrinter::reset() {
+  usedArrays.clear();
+  haveConstantArray = false;
+
+  /* Clear the PRODUCE_MODELS option if it was automatically set.
+   * We need to do this because the next query might not need the
+   * (get-value) SMT-LIBv2 command.
+   */
+  if (arraysToCallGetValueOn != NULL)
+    setSMTLIBboolOption(PRODUCE_MODELS, OPTION_DEFAULT);
+
+  arraysToCallGetValueOn = NULL;
+}
+
+bool ExprSMTLIBPrinter::isHumanReadable() { return humanReadable; }
+
+bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm) {
+  if (cdm > DECIMAL)
+    return false;
+
+  this->cdm = cdm;
+  return true;
+}
+
+void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) {
+  /* Handle simple boolean constants */
+
+  if (e->isTrue()) {
+    *p << "true";
+    return;
+  }
+
+  if (e->isFalse()) {
+    *p << "false";
+    return;
+  }
+
+  /* Handle bitvector constants */
+
+  std::string value;
+
+  /* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
+   * from the length of the string (e.g. zero is #b00000000). LLVM
+   * doesn't know about this so we need to pad the printed output
+   * with the appropriate number of zeros (zeroPad)
+   */
+  unsigned int zeroPad = 0;
 
-namespace ExprSMTLIBOptions
-{
-	//Command line options
-	llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> argConstantDisplayMode
-	("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated SMT-LIBv2 files (default=dec)"),
-	llvm::cl::values( clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin","Use binary form (e.g. #b00101101)"),
-					  clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex","Use Hexadecimal form (e.g. #x2D)"),
-					  clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec","Use decimal form (e.g. (_ bv45 8) )"),
-					  clEnumValEnd
-					),
-					llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL)
+  switch (cdm) {
+  case BINARY:
+    e->toString(value, 2);
+    *p << "#b";
 
+    zeroPad = e->getWidth() - value.length();
 
-	);
+    for (unsigned int count = 0; count < zeroPad; count++)
+      *p << "0";
 
-	llvm::cl::opt<bool> humanReadableSMTLIB("smtlib-human-readable",
-				llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"),
-				llvm::cl::init(false)
+    *p << value;
+    break;
 
+  case HEX:
+    e->toString(value, 16);
+    *p << "#x";
 
-	);
+    zeroPad = (e->getWidth() / 4) - value.length();
+    for (unsigned int count = 0; count < zeroPad; count++)
+      *p << "0";
 
+    *p << value;
+    break;
+
+  case DECIMAL:
+    e->toString(value, 10);
+    *p << "(_ bv" << value << " " << e->getWidth() << ")";
+    break;
+
+  default:
+    llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
+                    "display mode\n";
+  }
+}
+
+void ExprSMTLIBPrinter::printExpression(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
+  // check if casting might be necessary
+  if (getSort(e) != expectedSort) {
+    printCastToSort(e, expectedSort);
+    return;
+  }
+
+  switch (e->getKind()) {
+  case Expr::Constant:
+    printConstant(cast<ConstantExpr>(e));
+    return; // base case
+
+  case Expr::NotOptimized:
+    // skip to child
+    printExpression(e->getKid(0), expectedSort);
+    return;
+
+  case Expr::Read:
+    printReadExpr(cast<ReadExpr>(e));
+    return;
+
+  case Expr::Extract:
+    printExtractExpr(cast<ExtractExpr>(e));
+    return;
+
+  case Expr::SExt:
+  case Expr::ZExt:
+    printCastExpr(cast<CastExpr>(e));
+    return;
+
+  case Expr::Ne:
+    printNotEqualExpr(cast<NeExpr>(e));
+    return;
+
+  case Expr::Select:
+    // the if-then-else expression.
+    printSelectExpr(cast<SelectExpr>(e), expectedSort);
+    return;
+
+  case Expr::Eq:
+    /* The "=" operator is special in that it can take any sort but we must
+     * enforce that both arguments are the same type. We do this a lazy way
+     * by enforcing the second argument is of the same type as the first.
+     */
+    printSortArgsExpr(e, getSort(e->getKid(0)));
+
+    return;
+
+  case Expr::And:
+  case Expr::Or:
+  case Expr::Xor:
+  case Expr::Not:
+    /* These operators have a bitvector version and a bool version.
+     * For these operators only (e.g. wouldn't apply to bvult) if the expected
+     * sort the
+     * expression is T then that implies the arguments are also of type T.
+     */
+    printLogicalOrBitVectorExpr(e, expectedSort);
+
+    return;
+
+  default:
+    /* The remaining operators (Add,Sub...,Ult,Ule,..)
+     * Expect SORT_BITVECTOR arguments
+     */
+    printSortArgsExpr(e, SORT_BITVECTOR);
+    return;
+  }
+}
+
+void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr> &e) {
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent();
+
+  printSeperator();
+
+  // print array with updates recursively
+  printUpdatesAndArray(e->updates.head, e->updates.root);
+
+  // print index
+  printSeperator();
+  printExpression(e->index, SORT_BITVECTOR);
+
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr> &e) {
+  unsigned int lowIndex = e->offset;
+  unsigned int highIndex = lowIndex + e->width - 1;
+
+  *p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex
+     << ") ";
+
+  p->pushIndent(); // add indent for recursive call
+  printSeperator();
+
+  // recurse
+  printExpression(e->getKid(0), SORT_BITVECTOR);
+
+  p->popIndent(); // pop indent added for the recursive call
+  printSeperator();
+  *p << ")";
 }
 
+void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) {
+  /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
+   * instead of specifying of what bit-width we would like to extend to
+   * we specify how many bits to add to the child expression
+   *
+   * e.g
+   * ((_ sign_extend 64) (_ bv5 32))
+   *
+   * gives a (_ BitVec 96) instead of (_ BitVec 64)
+   *
+   * So we must work out how many bits we need to add.
+   *
+   * (e->width) is the desired number of bits
+   * (e->src->getWidth()) is the number of bits in the child
+   */
+  unsigned int numExtraBits = (e->width) - (e->src->getWidth());
+
+  *p << "((_ " << getSMTLIBKeyword(e) << " " << numExtraBits << ") ";
+
+  p->pushIndent(); // add indent for recursive call
+  printSeperator();
+
+  // recurse
+  printExpression(e->src, SORT_BITVECTOR);
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+
+  *p << ")";
+}
 
-namespace klee
-{
+void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr> &e) {
+  *p << "(not (";
+  p->pushIndent();
+  *p << "="
+     << " ";
+  p->pushIndent();
+  printSeperator();
+
+  /* The "=" operators allows both sorts. We assume
+   * that the second argument sort should be forced to be the same sort as the
+   * first argument
+   */
+  SMTLIB_SORT s = getSort(e->getKid(0));
+
+  printExpression(e->getKid(0), s);
+  printSeperator();
+  printExpression(e->getKid(1), s);
+  p->popIndent();
+  printSeperator();
+
+  *p << ")";
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
 
-	ExprSMTLIBPrinter::ExprSMTLIBPrinter() :
-		usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV),
-		humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL)
-	{
-		setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
-	}
+const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
+
+  switch (e->getKind()) {
+  case Expr::Read:
+    return "select";
+  case Expr::Select:
+    return "ite";
+  case Expr::Concat:
+    return "concat";
+  case Expr::Extract:
+    return "extract";
+  case Expr::ZExt:
+    return "zero_extend";
+  case Expr::SExt:
+    return "sign_extend";
+
+  case Expr::Add:
+    return "bvadd";
+  case Expr::Sub:
+    return "bvsub";
+  case Expr::Mul:
+    return "bvmul";
+  case Expr::UDiv:
+    return "bvudiv";
+  case Expr::SDiv:
+    return "bvsdiv";
+  case Expr::URem:
+    return "bvurem";
+  case Expr::SRem:
+    return "bvsrem";
+
+  /* And, Xor, Not and Or are not handled here because there different versions
+   * for different sorts. See printLogicalOrBitVectorExpr()
+   */
+
+  case Expr::Shl:
+    return "bvshl";
+  case Expr::LShr:
+    return "bvlshr";
+  case Expr::AShr:
+    return "bvashr";
+
+  case Expr::Eq:
+    return "=";
+
+  // Not Equal does not exist directly in SMTLIBv2
+
+  case Expr::Ult:
+    return "bvult";
+  case Expr::Ule:
+    return "bvule";
+  case Expr::Ugt:
+    return "bvugt";
+  case Expr::Uge:
+    return "bvuge";
+
+  case Expr::Slt:
+    return "bvslt";
+  case Expr::Sle:
+    return "bvsle";
+  case Expr::Sgt:
+    return "bvsgt";
+  case Expr::Sge:
+    return "bvsge";
+
+  default:
+    return "<error>";
+  }
+}
 
-	ExprSMTLIBPrinter::~ExprSMTLIBPrinter()
-	{
-		if(p!=NULL)
-			delete p;
-	}
+void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode *un,
+                                             const Array *root) {
+  if (un != NULL) {
+    *p << "(store ";
+    p->pushIndent();
+    printSeperator();
 
-	void ExprSMTLIBPrinter::setOutput(std::ostream& output)
-	{
-		o = &output;
-		if(p!=NULL)
-			delete p;
+    // recurse to get the array or update that this store operations applies to
+    printUpdatesAndArray(un->next, root);
 
-		p = new PrintContext(output);
-	}
+    printSeperator();
 
-	void ExprSMTLIBPrinter::setQuery(const Query& q)
-	{
-		query = &q;
-		reset(); // clear the data structures
-		scanAll();
-		negateQueryExpression();
-	}
+    // print index
+    printExpression(un->index, SORT_BITVECTOR);
+    printSeperator();
 
-	void ExprSMTLIBPrinter::reset()
-	{
-		usedArrays.clear();
-		haveConstantArray=false;
+    // print value that is assigned to this index of the array
+    printExpression(un->value, SORT_BITVECTOR);
 
-		/* Clear the PRODUCE_MODELS option if it was automatically set.
-		 * We need to do this because the next query might not need the
-		 * (get-value) SMT-LIBv2 command.
-		 */
-		if(arraysToCallGetValueOn !=NULL)
-			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_DEFAULT);
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+  } else {
+    // The base case of the recursion
+    *p << root->name;
+  }
+}
 
-		arraysToCallGetValueOn=NULL;
+void ExprSMTLIBPrinter::scanAll() {
+  // perform scan of all expressions
+  for (ConstraintManager::const_iterator i = query->constraints.begin();
+       i != query->constraints.end(); i++)
+    scan(*i);
 
+  // Scan the query too
+  scan(query->expr);
+}
+
+void ExprSMTLIBPrinter::generateOutput() {
+  if (p == NULL || query == NULL || o == NULL) {
+    llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
+                    "Output or query bad!\n";
+    return;
+  }
+
+  if (humanReadable)
+    printNotice();
+  printOptions();
+  printSetLogic();
+  printArrayDeclarations();
+  printConstraints();
+  printQuery();
+  printAction();
+  printExit();
+}
 
-	}
+void ExprSMTLIBPrinter::printSetLogic() {
+  *o << "(set-logic ";
+  switch (logicToUse) {
+  case QF_ABV:
+    *o << "QF_ABV";
+    break;
+  case QF_AUFBV:
+    *o << "QF_AUFBV";
+    break;
+  }
+  *o << " )\n";
+}
 
-	bool ExprSMTLIBPrinter::isHumanReadable()
-	{
-		return humanReadable;
-	}
+namespace {
 
-	bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm)
-	{
-		if(cdm > DECIMAL)
-			return false;
+struct ArrayPtrsByName {
+  bool operator()(const Array *a1, const Array *a2) const {
+    return a1->name < a2->name;
+  }
+};
 
-		this->cdm = cdm;
-		return true;
-	}
+}
 
-	void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr>& e)
-	{
-		/* Handle simple boolean constants */
-
-		if(e->isTrue())
-		{
-			*p << "true";
-			return;
-		}
-
-		if(e->isFalse())
-		{
-			*p << "false";
-			return;
-		}
-
-		/* Handle bitvector constants */
-
-		std::string value;
-
-		/* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
-		 * from the length of the string (e.g. zero is #b00000000). LLVM
-		 * doesn't know about this so we need to pad the printed output
-		 * with the appropriate number of zeros (zeroPad)
-		 */
-		unsigned int zeroPad=0;
-
-		switch(cdm)
-		{
-			case BINARY:
-				e->toString(value,2);
-				*p << "#b";
-
-				zeroPad = e->getWidth() - value.length();
-
-				for(unsigned int count=0; count < zeroPad; count++)
-					*p << "0";
-
-				*p << value ;
-				break;
-
-			case HEX:
-				e->toString(value,16);
-				*p << "#x";
-
-				zeroPad =  (e->getWidth() / 4) - value.length();
-				for(unsigned int count=0; count < zeroPad; count++)
-					*p << "0";
-
-				*p << value ;
-				break;
-
-			case DECIMAL:
-				e->toString(value,10);
-				*p << "(_ bv" << value<< " " << e->getWidth() << ")";
-				break;
-
-			default:
-				std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant display mode" << std::endl;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
-	{
-		//check if casting might be necessary
-		if(getSort(e) != expectedSort)
-		{
-			printCastToSort(e,expectedSort);
-			return;
-		}
-
-
-		switch(e->getKind())
-		{
-			case Expr::Constant:
-				printConstant(cast<ConstantExpr>(e));
-				return; //base case
-
-			case Expr::NotOptimized:
-				//skip to child
-				printExpression(e->getKid(0),expectedSort);
-				return;
-
-			case Expr::Read:
-				printReadExpr(cast<ReadExpr>(e));
-				return;
-
-			case Expr::Extract:
-				printExtractExpr(cast<ExtractExpr>(e));
-				return;
-
-			case Expr::SExt:
-			case Expr::ZExt:
-				printCastExpr(cast<CastExpr>(e));
-				return;
-
-			case Expr::Ne:
-				printNotEqualExpr(cast<NeExpr>(e));
-				return;
-
-			case Expr::Select:
-				//the if-then-else expression.
-				printSelectExpr(cast<SelectExpr>(e),expectedSort);
-				return;
-
-			case Expr::Eq:
-				/* The "=" operator is special in that it can take any sort but we must
-				 * enforce that both arguments are the same type. We do this a lazy way
-				 * by enforcing the second argument is of the same type as the first.
-				 */
-				printSortArgsExpr(e,getSort(e->getKid(0)));
-
-				return;
-
-			case Expr::And:
-			case Expr::Or:
-			case Expr::Xor:
-			case Expr::Not:
-				/* These operators have a bitvector version and a bool version.
-				 * For these operators only (e.g. wouldn't apply to bvult) if the expected sort the
-				 * expression is T then that implies the arguments are also of type T.
-				 */
-				printLogicalOrBitVectorExpr(e,expectedSort);
-
-				return;
-
-
-			default:
-				/* The remaining operators (Add,Sub...,Ult,Ule,..)
-				 * Expect SORT_BITVECTOR arguments
-				 */
-				printSortArgsExpr(e,SORT_BITVECTOR);
-				return;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr>& e)
-	{
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent();
-
-		printSeperator();
-
-		//print array with updates recursively
-		printUpdatesAndArray(e->updates.head,e->updates.root);
-
-		//print index
-		printSeperator();
-		printExpression(e->index,SORT_BITVECTOR);
-
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr>& e)
-	{
-		unsigned int lowIndex= e->offset;
-		unsigned int highIndex= lowIndex + e->width -1;
-
-		*p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex << ") ";
-
-		p->pushIndent(); //add indent for recursive call
-		printSeperator();
-
-		//recurse
-		printExpression(e->getKid(0),SORT_BITVECTOR);
-
-		p->popIndent(); //pop indent added for the recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr>& e)
-	{
-		/* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
-		 * instead of specifying of what bit-width we would like to extend to
-		 * we specify how many bits to add to the child expression
-		 *
-		 * e.g
-		 * ((_ sign_extend 64) (_ bv5 32))
-		 *
-		 * gives a (_ BitVec 96) instead of (_ BitVec 64)
-		 *
-		 * So we must work out how many bits we need to add.
-		 *
-		 * (e->width) is the desired number of bits
-		 * (e->src->getWidth()) is the number of bits in the child
-		 */
-		unsigned int numExtraBits= (e->width) - (e->src->getWidth());
-
-		*p << "((_ " << getSMTLIBKeyword(e) << " " <<
-				numExtraBits << ") ";
-
-		p->pushIndent(); //add indent for recursive call
-		printSeperator();
-
-		//recurse
-		printExpression(e->src,SORT_BITVECTOR);
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr>& e)
-	{
-		*p << "(not (";
-		p->pushIndent();
-		*p << "=" << " ";
-		p->pushIndent();
-		printSeperator();
-
-		/* The "=" operators allows both sorts. We assume
-		 * that the second argument sort should be forced to be the same sort as the
-		 * first argument
-		 */
-		SMTLIB_SORT s = getSort(e->getKid(0));
-
-		printExpression(e->getKid(0),s);
-		printSeperator();
-		printExpression(e->getKid(1),s);
-		p->popIndent();
-		printSeperator();
-
-		*p << ")";
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-	}
-
-
-	const char* ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr>& e)
-	{
-
-		switch(e->getKind())
-		{
-			case Expr::Read: return "select";
-			case Expr::Select: return "ite";
-			case Expr::Concat: return "concat";
-			case Expr::Extract: return "extract";
-			case Expr::ZExt: return "zero_extend";
-			case Expr::SExt: return "sign_extend";
-
-			case Expr::Add: return "bvadd";
-			case Expr::Sub: return "bvsub";
-			case Expr::Mul: return "bvmul";
-			case Expr::UDiv: return "bvudiv";
-			case Expr::SDiv: return "bvsdiv";
-			case Expr::URem: return "bvurem";
-			case Expr::SRem: return "bvsrem";
-
-
-			/* And, Xor, Not and Or are not handled here because there different versions
-			 * for different sorts. See printLogicalOrBitVectorExpr()
-			 */
-
-
-			case Expr::Shl: return "bvshl";
-			case Expr::LShr: return "bvlshr";
-			case Expr::AShr: return "bvashr";
-
-			case Expr::Eq: return "=";
-
-			//Not Equal does not exist directly in SMTLIBv2
-
-			case Expr::Ult: return "bvult";
-			case Expr::Ule: return "bvule";
-			case Expr::Ugt: return "bvugt";
-			case Expr::Uge: return "bvuge";
-
-			case Expr::Slt: return "bvslt";
-			case Expr::Sle: return "bvsle";
-			case Expr::Sgt: return "bvsgt";
-			case Expr::Sge: return "bvsge";
-
-			default:
-				return "<error>";
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode* un, const Array* root)
-	{
-		if(un!=NULL)
-		{
-			*p << "(store ";
-			p->pushIndent();
-			printSeperator();
-
-			//recurse to get the array or update that this store operations applies to
-			printUpdatesAndArray(un->next,root);
-
-			printSeperator();
-
-			//print index
-			printExpression(un->index,SORT_BITVECTOR);
-			printSeperator();
-
-			//print value that is assigned to this index of the array
-			printExpression(un->value,SORT_BITVECTOR);
-
-			p->popIndent();
-			printSeperator();
-			*p << ")";
-		}
-		else
-		{
-			//The base case of the recursion
-			*p << root->name;
-		}
-
-	}
-
-	void ExprSMTLIBPrinter::scanAll()
-	{
-		//perform scan of all expressions
-		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
-			scan(*i);
-
-		//Scan the query too
-		scan(query->expr);
-	}
-
-	void ExprSMTLIBPrinter::generateOutput()
-	{
-		if(p==NULL || query == NULL || o ==NULL)
-		{
-			std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. Output or query bad!" << std::endl;
-			return;
-		}
-
-		if(humanReadable) printNotice();
-		printOptions();
-		printSetLogic();
-		printArrayDeclarations();
-		printConstraints();
-		printQuery();
-		printAction();
-		printExit();
-	}
-
-	void ExprSMTLIBPrinter::printSetLogic()
-	{
-		*o << "(set-logic ";
-		switch(logicToUse)
-		{
-		case QF_ABV: *o << "QF_ABV"; break;
-		case QF_AUFBV: *o << "QF_AUFBV" ; break;
-		}
-		*o << " )" << std::endl;
-	}
-
-
-	void ExprSMTLIBPrinter::printArrayDeclarations()
-	{
-		//Assume scan() has been called
-		if(humanReadable)
-			*o << "; Array declarations" << endl;
-
-		//declare arrays
-		for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
-		{
-			*o << "(declare-fun " << (*it)->name << " () "
-				 "(Array (_ BitVec " << (*it)->getDomain() << ") "
-				 "(_ BitVec " << (*it)->getRange() << ") ) )" << endl;
-		}
-
-		//Set array values for constant values
-		if(haveConstantArray)
-		{
-			if(humanReadable)
-				*o << "; Constant Array Definitions" << endl;
-
-			const Array* array;
-
-			//loop over found arrays
-			for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
-			{
-				array= *it;
-				int byteIndex=0;
-				if(array->isConstantArray())
-				{
-					/*loop over elements in the array and generate an assert statement
-					  for each one
-					 */
-					for(vector< ref<ConstantExpr> >::const_iterator ce= array->constantValues.begin();
-							ce != array->constantValues.end(); ce++, byteIndex++)
-					{
-						*p << "(assert (";
-						p->pushIndent();
-						*p <<           "= ";
-						p->pushIndent();
-						printSeperator();
-
-						*p << "(select " << array->name << " (_ bv" << byteIndex << " " << array->getDomain() << ") )";
-						printSeperator();
-						printConstant((*ce));
-
-						p->popIndent();
-						printSeperator();
-						*p << ")";
-						p->popIndent();
-						printSeperator();
-						*p << ")";
-
-						p->breakLineI();
-
-					}
-				}
-			}
-		}
-	}
-
-	void ExprSMTLIBPrinter::printConstraints()
-	{
-		if(humanReadable)
-			*o << "; Constraints" << endl;
-
-		//Generate assert statements for each constraint
-		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
-		{
-			*p << "(assert ";
-			p->pushIndent();
-			printSeperator();
-
-			//recurse into Expression
-			printExpression(*i,SORT_BOOL);
-
-			p->popIndent();
-			printSeperator();
-			*p << ")"; p->breakLineI();
-		}
-
-	}
-
-	void ExprSMTLIBPrinter::printAction()
-	{
-		//Ask solver to check for satisfiability
-		*o << "(check-sat)" << endl;
-
-		/* If we has arrays to find the values of then we'll
-		 * ask the solver for the value of each bitvector in each array
-		 */
-		if(arraysToCallGetValueOn!=NULL && !arraysToCallGetValueOn->empty())
-		{
-
-			const Array* theArray=0;
-
-			//loop over the array names
-			for(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;
-				}
-
-			}
-
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::scan(const ref<Expr>& e)
-	{
-		if(e.isNull())
-		{
-			std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" << std::endl;
-			return;
-		}
-
-		if(isa<ConstantExpr>(e))
-			return; //we don't need to scan simple constants
-
-		if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
-		{
-
-			//Attempt to insert array and if array wasn't present before do more things
-			if(usedArrays.insert(re->updates.root).second)
-			{
-
-				//check if the array is constant
-				if( re->updates.root->isConstantArray())
-					haveConstantArray=true;
-
-				//scan the update list
-				scanUpdates(re->updates.head);
-
-			}
-
-		}
-
-		//recurse into the children
-		Expr* ep = e.get();
-		for(unsigned int i=0; i < ep->getNumKids(); i++)
-			scan(ep->getKid(i));
-	}
-
-
-	void ExprSMTLIBPrinter::scanUpdates(const UpdateNode* un)
-	{
-		while(un != NULL)
-		{
-			scan(un->index);
-			scan(un->value);
-			un= un->next;
-		}
-	}
-
-
-	void ExprSMTLIBPrinter::printExit()
-	{
-		*o << "(exit)" << endl;
-	}
-
-	bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l)
-	{
-		if(l > QF_AUFBV)
-			return false;
-
-		logicToUse=l;
-		return true;
-	}
-
-	void ExprSMTLIBPrinter::printSeperator()
-	{
-		if(humanReadable)
-			p->breakLineI();
-		else
-			p->write(" ");
-	}
-
-	void ExprSMTLIBPrinter::printNotice()
-	{
-		*o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
-	}
-
-	void ExprSMTLIBPrinter::setHumanReadable(bool hr)
-	{
-		humanReadable=hr;
-	}
-
-	void ExprSMTLIBPrinter::printOptions()
-	{
-		//Print out SMTLIBv2 boolean options
-		for(std::map<SMTLIBboolOptions,bool>::const_iterator i= smtlibBoolOptions.begin(); i!= smtlibBoolOptions.end(); i++)
-		{
-			*o << "(set-option :" << getSMTLIBOptionString(i->first) <<
-			" " << ((i->second)?"true":"false") << ")" << endl;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printQuery()
-	{
-		if(humanReadable)
-		{
-			*p << "; Query from solver turned into an assert";
-			p->breakLineI();
-		}
-
-		p->pushIndent();
-		*p << "(assert";
-		p->pushIndent();
-		printSeperator();
-
-		printExpression(queryAssert,SORT_BOOL);
-
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-		p->popIndent();
-		p->breakLineI();
-	}
-
-	ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr>& e)
-	{
-		/* We could handle every operator in a large switch statement,
-		 * but this seems more elegant.
-		 */
-
-		if(e->getKind() == Expr::Extract)
-		{
-			/* This is a special corner case. In most cases if a node in the expression tree
-			 * is of width 1 it should be considered as SORT_BOOL. However it is possible to
-			 * perform an extract operation on a SORT_BITVECTOR and produce a SORT_BITVECTOR of length 1.
-			 * The ((_ extract i j) () ) operation in SMTLIBv2 always produces SORT_BITVECTOR
-			 */
-			return SORT_BITVECTOR;
-		}
-		else
-			return (e->getWidth() == Expr::Bool)?(SORT_BOOL):(SORT_BITVECTOR);
-	}
-
-	void ExprSMTLIBPrinter::printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
-	{
-		switch(sort)
-		{
-			case SORT_BITVECTOR:
-				if(humanReadable)
-				{
-					p->breakLineI(); *p << ";Performing implicit bool to bitvector cast"; p->breakLine();
-				}
-				//We assume the e is a bool that we need to cast to a bitvector sort.
-				*p << "(ite"; p->pushIndent(); printSeperator();
-				printExpression(e,SORT_BOOL); printSeperator();
-				*p << "(_ bv1 1)" ; printSeperator(); //printing the "true" bitvector
-				*p << "(_ bv0 1)" ; p->popIndent(); printSeperator(); //printing the "false" bitvector
-				*p << ")";
-				break;
-			case SORT_BOOL:
-			{
-				/* We make the assumption (might be wrong) that any bitvector whos unsigned decimal value is
-				 * is zero is interpreted as "false", otherwise it is true.
-				 *
-				 * This may not be the interpretation we actually want!
-				 */
-				Expr::Width bitWidth=e->getWidth();
-				if(humanReadable)
-				{
-					p->breakLineI(); *p << ";Performing implicit bitvector to bool cast"; p->breakLine();
-				}
-				*p << "(bvugt"; p->pushIndent(); printSeperator();
-				// We assume is e is a bitvector
-				printExpression(e,SORT_BITVECTOR); printSeperator();
-				*p << "(_ bv0 " << bitWidth << ")"; p->popIndent(); printSeperator(); //Zero bitvector of required width
-				*p << ")";
-
-				if(bitWidth!=Expr::Bool)
-					std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " << bitWidth << ") to bool!" << std::endl;
-
-			}
-				break;
-			default:
-				assert(0 && "Unsupported cast!");
-		}
-	}
-
-	void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		//This is the if-then-else expression
-
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent(); //add indent for recursive call
-
-			//The condition
-			printSeperator();
-			printExpression(e->getKid(0),SORT_BOOL);
-
-			/* This operator is special in that the remaining children
-			 * can be of any sort.
-			 */
-
-			//if true
-			printSeperator();
-			printExpression(e->getKid(1),s);
-
-			//if false
-			printSeperator();
-			printExpression(e->getKid(2),s);
-
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent(); //add indent for recursive call
-
-		//loop over children and recurse into each expecting they are of sort "s"
-		for(unsigned int i=0; i < e->getNumKids(); i++)
-		{
-			printSeperator();
-			printExpression(e->getKid(i),s);
-		}
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		/* For these operators it is the case that the expected sort is the same as the sorts
-		 * of the arguments.
-		 */
-
-		*p << "(";
-		switch(e->getKind())
-		{
-			case Expr::And:
-				*p << ((s==SORT_BITVECTOR)?"bvand":"and");
-				break;
-			case Expr::Not:
-				*p << ((s==SORT_BITVECTOR)?"bvnot":"not");
-				break;
-			case Expr::Or:
-				*p << ((s==SORT_BITVECTOR)?"bvor":"or");
-				break;
-
-			case Expr::Xor:
-				*p << ((s==SORT_BITVECTOR)?"bvxor":"xor");
-				break;
-			default:
-				*p << "ERROR"; // this shouldn't happen
-		}
-		*p << " ";
-
-		p->pushIndent(); //add indent for recursive call
-
-		//loop over children and recurse into each expecting they are of sort "s"
-		for(unsigned int i=0; i < e->getNumKids(); i++)
-		{
-			printSeperator();
-			printExpression(e->getKid(i),s);
-		}
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::negateQueryExpression()
-	{
-		//Negating the query
-		queryAssert = Expr::createIsZero(query->expr);
-	}
-
-	bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value)
-	{
-		std::pair< std::map<SMTLIBboolOptions,bool>::iterator, bool> thePair;
-		bool theValue=  (value==OPTION_TRUE)?true:false;
-
-		switch(option)
-		{
-			case PRINT_SUCCESS:
-			case PRODUCE_MODELS:
-			case INTERACTIVE_MODE:
-				thePair=smtlibBoolOptions.insert(std::pair<SMTLIBboolOptions,bool>(option,theValue));
-
-				if(value== OPTION_DEFAULT)
-				{
-					//we should unset (by removing from map) this option so the solver uses its default
-					smtlibBoolOptions.erase(thePair.first);
-					return true;
-				}
-
-				if(!thePair.second)
-				{
-					//option was already present so modify instead.
-					thePair.first->second=value;
-				}
-				return true;
-			default:
-				return false;
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array*>& a)
-	{
-		arraysToCallGetValueOn = &a;
-
-		//This option must be set in order to use the SMTLIBv2 command (get-value () )
-		if(!a.empty())
-			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_TRUE);
-
-		/* There is a risk that users will ask about array values that aren't
-		 * even in the query. We should add them to the usedArrays list and hope
-		 * 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)
-		{
-			usedArrays.insert(*i);
-		}
-
-	}
-
-const char* ExprSMTLIBPrinter::getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option)
-{
-	switch(option)
-	{
-		case PRINT_SUCCESS: return "print-success";
-		case PRODUCE_MODELS: return "produce-models";
-		case INTERACTIVE_MODE: return "interactive-mode";
-		default:
-			return "unknown-option";
-	}
+void ExprSMTLIBPrinter::printArrayDeclarations() {
+  // Assume scan() has been called
+  if (humanReadable)
+    *o << "; Array declarations\n";
+
+  // Declare arrays in a deterministic order.
+  std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
+  std::sort(sortedArrays.begin(), sortedArrays.end(), ArrayPtrsByName());
+  for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+       it != sortedArrays.end(); it++) {
+    *o << "(declare-fun " << (*it)->name << " () "
+                                            "(Array (_ BitVec "
+       << (*it)->getDomain() << ") "
+                                "(_ BitVec " << (*it)->getRange() << ") ) )"
+       << "\n";
+  }
+
+  // Set array values for constant values
+  if (haveConstantArray) {
+    if (humanReadable)
+      *o << "; Constant Array Definitions\n";
+
+    const Array *array;
+
+    // loop over found arrays
+    for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+         it != sortedArrays.end(); it++) {
+      array = *it;
+      int byteIndex = 0;
+      if (array->isConstantArray()) {
+        /*loop over elements in the array and generate an assert statement
+          for each one
+         */
+        for (std::vector<ref<ConstantExpr> >::const_iterator
+                 ce = array->constantValues.begin();
+             ce != array->constantValues.end(); ce++, byteIndex++) {
+          *p << "(assert (";
+          p->pushIndent();
+          *p << "= ";
+          p->pushIndent();
+          printSeperator();
+
+          *p << "(select " << array->name << " (_ bv" << byteIndex << " "
+             << array->getDomain() << ") )";
+          printSeperator();
+          printConstant((*ce));
+
+          p->popIndent();
+          printSeperator();
+          *p << ")";
+          p->popIndent();
+          printSeperator();
+          *p << ")";
+
+          p->breakLineI();
+        }
+      }
+    }
+  }
 }
 
+void ExprSMTLIBPrinter::printConstraints() {
+  if (humanReadable)
+    *o << "; Constraints\n";
+
+  // Generate assert statements for each constraint
+  for (ConstraintManager::const_iterator i = query->constraints.begin();
+       i != query->constraints.end(); i++) {
+    *p << "(assert ";
+    p->pushIndent();
+    printSeperator();
+
+    // recurse into Expression
+    printExpression(*i, SORT_BOOL);
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    p->breakLineI();
+  }
 }
 
+void ExprSMTLIBPrinter::printAction() {
+  // Ask solver to check for satisfiability
+  *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
+   */
+  if (arraysToCallGetValueOn != NULL && !arraysToCallGetValueOn->empty()) {
+
+    const Array *theArray = 0;
+
+    // loop over the array names
+    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() << ") ) ) )\n";
+      }
+    }
+  }
+}
 
+void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
+  if (e.isNull()) {
+    llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
+                 << "\n";
+    return;
+  }
 
+  if (isa<ConstantExpr>(e))
+    return; // we don't need to scan simple constants
+
+  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+
+    // Attempt to insert array and if array wasn't present before do more things
+    if (usedArrays.insert(re->updates.root).second) {
+
+      // check if the array is constant
+      if (re->updates.root->isConstantArray())
+        haveConstantArray = true;
+
+      // scan the update list
+      scanUpdates(re->updates.head);
+    }
+  }
+
+  // recurse into the children
+  Expr *ep = e.get();
+  for (unsigned int i = 0; i < ep->getNumKids(); i++)
+    scan(ep->getKid(i));
+}
+
+void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
+  while (un != NULL) {
+    scan(un->index);
+    scan(un->value);
+    un = un->next;
+  }
+}
+
+void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; }
+
+bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) {
+  if (l > QF_AUFBV)
+    return false;
+
+  logicToUse = l;
+  return true;
+}
+
+void ExprSMTLIBPrinter::printSeperator() {
+  if (humanReadable)
+    p->breakLineI();
+  else
+    p->write(" ");
+}
+
+void ExprSMTLIBPrinter::printNotice() {
+  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n";
+}
+
+void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; }
+
+void ExprSMTLIBPrinter::printOptions() {
+  // Print out SMTLIBv2 boolean options
+  for (std::map<SMTLIBboolOptions, bool>::const_iterator i =
+           smtlibBoolOptions.begin();
+       i != smtlibBoolOptions.end(); i++) {
+    *o << "(set-option :" << getSMTLIBOptionString(i->first) << " "
+       << ((i->second) ? "true" : "false") << ")\n";
+  }
+}
+
+void ExprSMTLIBPrinter::printQuery() {
+  if (humanReadable) {
+    *p << "; Query from solver turned into an assert";
+    p->breakLineI();
+  }
+
+  p->pushIndent();
+  *p << "(assert";
+  p->pushIndent();
+  printSeperator();
+
+  printExpression(queryAssert, SORT_BOOL);
+
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+  p->popIndent();
+  p->breakLineI();
+}
+
+ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr> &e) {
+  switch (e->getKind()) {
+  case Expr::NotOptimized:
+    return getSort(e->getKid(0));
+
+  // The relational operators are bools.
+  case Expr::Eq:
+  case Expr::Ne:
+  case Expr::Slt:
+  case Expr::Sle:
+  case Expr::Sgt:
+  case Expr::Sge:
+  case Expr::Ult:
+  case Expr::Ule:
+  case Expr::Ugt:
+  case Expr::Uge:
+    return SORT_BOOL;
+
+  // These may be bitvectors or bools depending on their width (see
+  // printConstant and printLogicalOrBitVectorExpr).
+  case Expr::Constant:
+  case Expr::And:
+  case Expr::Not:
+  case Expr::Or:
+  case Expr::Xor:
+    return e->getWidth() == Expr::Bool ? SORT_BOOL : SORT_BITVECTOR;
+
+  // Everything else is a bitvector.
+  default:
+    return SORT_BITVECTOR;
+  }
+}
+
+void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e,
+                                        ExprSMTLIBPrinter::SMTLIB_SORT sort) {
+  switch (sort) {
+  case SORT_BITVECTOR:
+    if (humanReadable) {
+      p->breakLineI();
+      *p << ";Performing implicit bool to bitvector cast";
+      p->breakLine();
+    }
+    // We assume the e is a bool that we need to cast to a bitvector sort.
+    *p << "(ite";
+    p->pushIndent();
+    printSeperator();
+    printExpression(e, SORT_BOOL);
+    printSeperator();
+    *p << "(_ bv1 1)";
+    printSeperator(); // printing the "true" bitvector
+    *p << "(_ bv0 1)";
+    p->popIndent();
+    printSeperator(); // printing the "false" bitvector
+    *p << ")";
+    break;
+  case SORT_BOOL: {
+    /* We make the assumption (might be wrong) that any bitvector whos unsigned
+     *decimal value is
+     * is zero is interpreted as "false", otherwise it is true.
+     *
+     * This may not be the interpretation we actually want!
+     */
+    Expr::Width bitWidth = e->getWidth();
+    if (humanReadable) {
+      p->breakLineI();
+      *p << ";Performing implicit bitvector to bool cast";
+      p->breakLine();
+    }
+    *p << "(bvugt";
+    p->pushIndent();
+    printSeperator();
+    // We assume is e is a bitvector
+    printExpression(e, SORT_BITVECTOR);
+    printSeperator();
+    *p << "(_ bv0 " << bitWidth << ")";
+    p->popIndent();
+    printSeperator(); // Zero bitvector of required width
+    *p << ")";
+
+    if (bitWidth != Expr::Bool)
+      llvm::errs()
+          << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
+          << bitWidth << ") to bool!\n";
+
+  } break;
+  default:
+    assert(0 && "Unsupported cast!");
+  }
+}
+
+void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr> &e,
+                                        ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  // This is the if-then-else expression
+
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent(); // add indent for recursive call
+
+  // The condition
+  printSeperator();
+  printExpression(e->getKid(0), SORT_BOOL);
+
+  /* This operator is special in that the remaining children
+   * can be of any sort.
+   */
+
+  // if true
+  printSeperator();
+  printExpression(e->getKid(1), s);
+
+  // if false
+  printSeperator();
+  printExpression(e->getKid(2), s);
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr> &e,
+                                          ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent(); // add indent for recursive call
+
+  // loop over children and recurse into each expecting they are of sort "s"
+  for (unsigned int i = 0; i < e->getNumKids(); i++) {
+    printSeperator();
+    printExpression(e->getKid(i), s);
+  }
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  /* For these operators it is the case that the expected sort is the same as
+   * the sorts
+   * of the arguments.
+   */
+
+  *p << "(";
+  switch (e->getKind()) {
+  case Expr::And:
+    *p << ((s == SORT_BITVECTOR) ? "bvand" : "and");
+    break;
+  case Expr::Not:
+    *p << ((s == SORT_BITVECTOR) ? "bvnot" : "not");
+    break;
+  case Expr::Or:
+    *p << ((s == SORT_BITVECTOR) ? "bvor" : "or");
+    break;
+
+  case Expr::Xor:
+    *p << ((s == SORT_BITVECTOR) ? "bvxor" : "xor");
+    break;
+  default:
+    *p << "ERROR"; // this shouldn't happen
+  }
+  *p << " ";
+
+  p->pushIndent(); // add indent for recursive call
+
+  // loop over children and recurse into each expecting they are of sort "s"
+  for (unsigned int i = 0; i < e->getNumKids(); i++) {
+    printSeperator();
+    printExpression(e->getKid(i), s);
+  }
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::negateQueryExpression() {
+  // Negating the query
+  queryAssert = Expr::createIsZero(query->expr);
+}
+
+bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option,
+                                            SMTLIBboolValues value) {
+  std::pair<std::map<SMTLIBboolOptions, bool>::iterator, bool> thePair;
+  bool theValue = (value == OPTION_TRUE) ? true : false;
+
+  switch (option) {
+  case PRINT_SUCCESS:
+  case PRODUCE_MODELS:
+  case INTERACTIVE_MODE:
+    thePair = smtlibBoolOptions.insert(
+        std::pair<SMTLIBboolOptions, bool>(option, theValue));
+
+    if (value == OPTION_DEFAULT) {
+      // we should unset (by removing from map) this option so the solver uses
+      // its default
+      smtlibBoolOptions.erase(thePair.first);
+      return true;
+    }
+
+    if (!thePair.second) {
+      // option was already present so modify instead.
+      thePair.first->second = value;
+    }
+    return true;
+  default:
+    return false;
+  }
+}
+
+void
+ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) {
+  arraysToCallGetValueOn = &a;
+
+  // This option must be set in order to use the SMTLIBv2 command (get-value ()
+  // )
+  if (!a.empty())
+    setSMTLIBboolOption(PRODUCE_MODELS, OPTION_TRUE);
+
+  /* There is a risk that users will ask about array values that aren't
+   * even in the query. We should add them to the usedArrays list and hope
+   * that the solver knows what to do when we ask for the values of arrays
+   * that don't feature in our query!
+   */
+  for (std::vector<const Array *>::const_iterator i = a.begin(); i != a.end();
+       ++i) {
+    usedArrays.insert(*i);
+  }
+}
+
+const char *ExprSMTLIBPrinter::getSMTLIBOptionString(
+    ExprSMTLIBPrinter::SMTLIBboolOptions option) {
+  switch (option) {
+  case PRINT_SUCCESS:
+    return "print-success";
+  case PRODUCE_MODELS:
+    return "produce-models";
+  case INTERACTIVE_MODE:
+    return "interactive-mode";
+  default:
+    return "unknown-option";
+  }
+}
+}
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/Makefile b/lib/Expr/Makefile
index b80569b3..25557600 100644
--- a/lib/Expr/Makefile
+++ b/lib/Expr/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleaverExpr
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
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/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 14fd8308..bf7049ba 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -22,8 +22,12 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
     next(_next),
     index(_index),
     value(_value) {
+  // FIXME: What we need to check here instead is that _value is of the same width 
+  // as the range of the array that the update node is part of.
+  /*
   assert(_value->getWidth() == Expr::Int8 && 
          "Update value should be 8-bit wide.");
+  */
   computeHash();
   if (next) {
     ++next->refCount;
@@ -84,6 +88,12 @@ UpdateList &UpdateList::operator=(const UpdateList &b) {
 }
 
 void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
+  
+  if (root) {
+    assert(root->getDomain() == index->getWidth());
+    assert(root->getRange() == value->getWidth());
+  }
+
   if (head) --head->refCount;
   head = new UpdateNode(head, index, value);
   ++head->refCount;
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 79fd4afc..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;
@@ -83,7 +82,12 @@ bool DivCheckPass::runOnModule(Module &M) {
               divZeroCheckFunction = cast<Function>(fc);
             }
 
-	    CallInst::Create(divZeroCheckFunction, denominator, "", &*i);
+            CallInst * ci = CallInst::Create(divZeroCheckFunction, denominator, "", &*i);
+
+            // Set debug location of checking call to that of the div/rem
+            // operation so error locations are reported in the correct
+            // location.
+            ci->setDebugLoc(binOp->getDebugLoc());
             moduleChanged = true;
           }
         }
@@ -138,11 +142,14 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
             }
 
             // Inject CallInstr to check if overshifting possible
+            CallInst* ci =
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
             CallInst::Create(overshiftCheckFunction, args, "", &*i);
 #else
             CallInst::Create(overshiftCheckFunction, args.begin(), args.end(), "", &*i);
 #endif
+            // set debug information from binary operand to preserve it
+            ci->setDebugLoc(binOp->getDebugLoc());
             moduleChanged = true;
           }
         }
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 301db1ff..19d7e511 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -33,6 +33,7 @@
 #include "llvm/Analysis/DebugInfo.h"
 #endif
 #include "llvm/Analysis/ValueTracking.h"
+#include "llvm/Support/Debug.h"
 
 #include <map>
 #include <string>
@@ -108,64 +109,35 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
 
   for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
        fnIt != fn_ie; ++fnIt) {
-    const std::string *initialFile = &dummyString;
-    unsigned initialLine = 0;
-
-    // It may be better to look for the closest stoppoint to the entry
-    // following the CFG, but it is not clear that it ever matters in
-    // practice.
-    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt);
-         it != ie; ++it)
-      if (getInstructionDebugInfo(&*it, initialFile, initialLine))
-        break;
-    
-    typedef std::map<BasicBlock*, std::pair<const std::string*,unsigned> > 
-      sourceinfo_ty;
-    sourceinfo_ty sourceInfo;
-    for (llvm::Function::iterator bbIt = fnIt->begin(), bbie = fnIt->end(); 
-         bbIt != bbie; ++bbIt) {
-      std::pair<sourceinfo_ty::iterator, bool>
-        res = sourceInfo.insert(std::make_pair(bbIt,
-                                               std::make_pair(initialFile,
-                                                              initialLine)));
-      if (!res.second)
-        continue;
-
-      std::vector<BasicBlock*> worklist;
-      worklist.push_back(bbIt);
-
-      do {
-        BasicBlock *bb = worklist.back();
-        worklist.pop_back();
-
-        sourceinfo_ty::iterator si = sourceInfo.find(bb);
-        assert(si != sourceInfo.end());
-        const std::string *file = si->second.first;
-        unsigned line = si->second.second;
-        
-        for (BasicBlock::iterator it = bb->begin(), ie = bb->end();
-             it != ie; ++it) {
-          Instruction *instr = it;
-          unsigned assemblyLine = 0;
-          std::map<const Instruction*, unsigned>::const_iterator ltit = 
-            lineTable.find(instr);
-          if (ltit!=lineTable.end())
-            assemblyLine = ltit->second;
-          getInstructionDebugInfo(instr, file, line);
-          infos.insert(std::make_pair(instr,
-                                      InstructionInfo(id++,
-                                                      *file,
-                                                      line,
-                                                      assemblyLine)));        
-        }
-        
-        for (succ_iterator it = succ_begin(bb), ie = succ_end(bb); 
-             it != ie; ++it) {
-          if (sourceInfo.insert(std::make_pair(*it,
-                                               std::make_pair(file, line))).second)
-            worklist.push_back(*it);
-        }
-      } while (!worklist.empty());
+
+    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie;
+        ++it) {
+      const std::string *initialFile = &dummyString;
+      unsigned initialLine = 0;
+      Instruction *instr = &*it;
+      unsigned assemblyLine = 0;
+
+      std::map<const Instruction*, unsigned>::const_iterator ltit =
+        lineTable.find(instr);
+      if (ltit!=lineTable.end())
+        assemblyLine = ltit->second;
+      if (getInstructionDebugInfo(instr, initialFile, initialLine))
+      {
+        infos.insert(std::make_pair(instr,
+                                    InstructionInfo(id++,
+                                                    *initialFile,
+                                                    initialLine,
+                                                    assemblyLine)));
+        DEBUG_WITH_TYPE("klee_obtained_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") has debug location " << *initialFile << ":" << initialLine << "\n");
+      }
+      else
+      {
+        DEBUG_WITH_TYPE("klee_missing_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") is missing debug info.\n");
+      }
     }
   }
 }
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index d889b51f..697b6ea9 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -182,7 +182,8 @@ static void injectStaticConstructorsAndDestructors(Module *m) {
   
   if (ctors || dtors) {
     Function *mainFn = m->getFunction("main");
-    assert(mainFn && "unable to find main function");
+    if (!mainFn)
+      klee_error("Could not find main() function.");
 
     if (ctors)
     CallInst::Create(getStubFunctionForCtorList(m, ctors, "klee.ctor_stub"),
@@ -229,7 +230,7 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType,
 /// It is intended that this function be used for inling calls to
 /// check functions like <tt>klee_div_zero_check()</tt>
 static void inlineChecks(Module *module, const char * functionName) {
-  std::vector<CallInst*> checkCalls;
+  std::vector<CallSite> checkCalls;
     Function* runtimeCheckCall = module->getFunction(functionName);
     if (runtimeCheckCall == 0)
     {
@@ -237,22 +238,19 @@ static void inlineChecks(Module *module, const char * functionName) {
       return;
     }
 
-    // Iterate through instructions in module and collect all
-    // call instructions to "functionName" that we care about.
-    for (Module::iterator f = module->begin(), fe = module->end(); f != fe; ++f) {
-      for (inst_iterator i=inst_begin(f), ie = inst_end(f); i != ie; ++i) {
-        if ( CallInst* ci = dyn_cast<CallInst>(&*i) )
-        {
-          if ( ci->getCalledFunction() == runtimeCheckCall)
-            checkCalls.push_back(ci);
-        }
+    for (Value::use_iterator i = runtimeCheckCall->use_begin(),
+        e = runtimeCheckCall->use_end(); i != e; ++i)
+      if (isa<InvokeInst>(*i) || isa<CallInst>(*i)) {
+        CallSite cs(*i);
+        if (!cs.getCalledFunction())
+          continue;
+        checkCalls.push_back(cs);
       }
-    }
 
     unsigned int successCount=0;
     unsigned int failCount=0;
     InlineFunctionInfo IFI(0,0);
-    for ( std::vector<CallInst*>::iterator ci = checkCalls.begin(),
+    for ( std::vector<CallSite>::iterator ci = checkCalls.begin(),
           cie = checkCalls.end();
           ci != cie; ++ci)
     {
@@ -269,6 +267,17 @@ static void inlineChecks(Module *module, const char * functionName) {
     DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) );
 }
 
+void KModule::addInternalFunction(const char* functionName){
+  Function* internalFunction = module->getFunction(functionName);
+  if (!internalFunction) {
+    DEBUG_WITH_TYPE("KModule", klee_warning(
+        "Failed to add internal function %s. Not found.", functionName));
+    return ;
+  }
+  DEBUG( klee_message("Added function %s.",functionName));
+  internalFunctions.insert(internalFunction);
+}
+
 void KModule::prepare(const Interpreter::ModuleOptions &opts,
                       InterpreterHandler *ih) {
   if (!MergeAtExit.empty()) {
@@ -366,25 +375,23 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   // FIXME: Find a way that we can test programs without requiring
   // this to be linked in, it makes low level debugging much more
   // annoying.
-  llvm::sys::Path path(opts.LibraryDir);
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
-  path.appendComponent("kleeRuntimeIntrinsic.bc");
+
+  SmallString<128> LibPath(opts.LibraryDir);
+  llvm::sys::path::append(LibPath,
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3,3)
+      "kleeRuntimeIntrinsic.bc"
 #else
-  path.appendComponent("libkleeRuntimeIntrinsic.bca");
+      "libkleeRuntimeIntrinsic.bca"
 #endif
-  module = linkWithLibrary(module, path.c_str());
-
-  /* In order for KLEE to report ALL errors at instrumented
-   * locations the instrumentation call (e.g. "klee_div_zero_check")
-   * must be inlined. Otherwise one of the instructions in the
-   * instrumentation function will be used as the the location of
-   * the error which means that the error cannot be recorded again
-   * ( unless -emit-all-errors is used).
-   */
+    );
+  module = linkWithLibrary(module, LibPath.str());
+
+  // Add internal functions which are not used to check if instructions
+  // have been already visited
   if (opts.CheckDivZero)
-    inlineChecks(module, "klee_div_zero_check");
+    addInternalFunction("klee_div_zero_check");
   if (opts.CheckOvershift)
-    inlineChecks(module, "klee_overshift_check");
+    addInternalFunction("klee_overshift_check");
 
 
   // Needs to happen after linking (since ctors/dtors can be modified)
@@ -423,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);
@@ -442,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/Makefile b/lib/Module/Makefile
index bfd7c469..091a7d45 100755
--- a/lib/Module/Makefile
+++ b/lib/Module/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeModule
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index fcdfa35a..d00cf574 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -9,6 +9,13 @@
 
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Config/Version.h"
+// FIXME: This does not belong here.
+#include "../Core/Common.h"
+#include "../Core/SpecialFunctionHandler.h"
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 4)
+#include "llvm/IR/LLVMContext.h"
+#endif
 
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/Bitcode/ReaderWriter.h"
@@ -17,6 +24,11 @@
 #include "llvm/IR/IntrinsicInst.h"
 #include "llvm/IRReader/IRReader.h"
 #include "llvm/IR/Module.h"
+#include "llvm/Object/Archive.h"
+#include "llvm/Object/ObjectFile.h"
+#include "llvm/Object/Error.h"
+#include "llvm/Support/FileSystem.h"
+#include "llvm/IR/ValueSymbolTable.h"
 #include "llvm/Support/SourceMgr.h"
 #include "llvm/Support/DataStream.h"
 #else
@@ -30,13 +42,14 @@
 #include "llvm/Assembly/AssemblyAnnotationWriter.h"
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/CallSite.h"
+#include "llvm/Support/Debug.h"
 #include "llvm/Support/InstIterator.h"
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Analysis/ValueTracking.h"
 #include "llvm/Support/Path.h"
 
 #include <map>
-#include <iostream>
+#include <set>
 #include <fstream>
 #include <sstream>
 #include <string>
@@ -44,18 +57,349 @@
 using namespace llvm;
 using namespace klee;
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+/// Based on GetAllUndefinedSymbols() from LLVM3.2
+///
+/// GetAllUndefinedSymbols - calculates the set of undefined symbols that still
+/// exist in an LLVM module. This is a bit tricky because there may be two
+/// symbols with the same name but different LLVM types that will be resolved to
+/// each other but aren't currently (thus we need to treat it as resolved).
+///
+/// Inputs:
+///  M - The module in which to find undefined symbols.
+///
+/// Outputs:
+///  UndefinedSymbols - A set of C++ strings containing the name of all
+///                     undefined symbols.
+///
+static void
+GetAllUndefinedSymbols(Module *M, std::set<std::string> &UndefinedSymbols) {
+  static const std::string llvmIntrinsicPrefix="llvm.";
+  std::set<std::string> DefinedSymbols;
+  UndefinedSymbols.clear();
+  DEBUG_WITH_TYPE("klee_linker", dbgs() << "*** Computing undefined symbols ***\n");
+
+  for (Module::iterator I = M->begin(), E = M->end(); I != E; ++I)
+    if (I->hasName()) {
+      if (I->isDeclaration())
+        UndefinedSymbols.insert(I->getName());
+      else if (!I->hasLocalLinkage()) {
+        assert(!I->hasDLLImportLinkage()
+               && "Found dllimported non-external symbol!");
+        DefinedSymbols.insert(I->getName());
+      }
+    }
+
+  for (Module::global_iterator I = M->global_begin(), E = M->global_end();
+       I != E; ++I)
+    if (I->hasName()) {
+      if (I->isDeclaration())
+        UndefinedSymbols.insert(I->getName());
+      else if (!I->hasLocalLinkage()) {
+        assert(!I->hasDLLImportLinkage()
+               && "Found dllimported non-external symbol!");
+        DefinedSymbols.insert(I->getName());
+      }
+    }
+
+  for (Module::alias_iterator I = M->alias_begin(), E = M->alias_end();
+       I != E; ++I)
+    if (I->hasName())
+      DefinedSymbols.insert(I->getName());
+
+
+  // Prune out any defined symbols from the undefined symbols set
+  // and other symbols we don't want to treat as an undefined symbol
+  std::vector<std::string> SymbolsToRemove;
+  for (std::set<std::string>::iterator I = UndefinedSymbols.begin();
+       I != UndefinedSymbols.end(); ++I )
+  {
+    if (DefinedSymbols.count(*I))
+    {
+      SymbolsToRemove.push_back(*I);
+      continue;
+    }
+
+    // Strip out llvm intrinsics
+    if ( (I->size() >= llvmIntrinsicPrefix.size() ) &&
+       (I->compare(0, llvmIntrinsicPrefix.size(), llvmIntrinsicPrefix) == 0) )
+    {
+      DEBUG_WITH_TYPE("klee_linker", dbgs() << "LLVM intrinsic " << *I <<
+                      " has will be removed from undefined symbols"<< "\n");
+      SymbolsToRemove.push_back(*I);
+      continue;
+    }
+
+    // Symbol really is undefined
+    DEBUG_WITH_TYPE("klee_linker", dbgs() << "Symbol " << *I << " is undefined.\n");
+  }
+
+  // Remove KLEE intrinsics from set of undefined symbols
+  for (SpecialFunctionHandler::const_iterator sf = SpecialFunctionHandler::begin(),
+       se = SpecialFunctionHandler::end(); sf != se; ++sf)
+  {
+    if (UndefinedSymbols.find(sf->name) == UndefinedSymbols.end())
+      continue;
+
+    SymbolsToRemove.push_back(sf->name);
+    DEBUG_WITH_TYPE("klee_linker", dbgs() << "KLEE intrinsic " << sf->name <<
+                    " has will be removed from undefined symbols"<< "\n");
+  }
+
+  // Now remove the symbols from undefined set.
+  for (size_t i = 0, j = SymbolsToRemove.size(); i < j; ++i )
+    UndefinedSymbols.erase(SymbolsToRemove[i]);
+
+  DEBUG_WITH_TYPE("klee_linker", dbgs() << "*** Finished computing undefined symbols ***\n");
+}
+
+
+/*!  A helper function for linkBCA() which cleans up
+ *   memory allocated by that function.
+ */
+static void CleanUpLinkBCA(std::vector<Module*> &archiveModules)
+{
+  for (std::vector<Module*>::iterator I = archiveModules.begin(), E = archiveModules.end();
+      I != E; ++I)
+  {
+    delete (*I);
+  }
+}
+
+/*! A helper function for klee::linkWithLibrary() that links in an archive of bitcode
+ *  modules into a composite bitcode module
+ *
+ *  \param[in] archive Archive of bitcode modules
+ *  \param[in,out] composite The bitcode module to link against the archive
+ *  \param[out] errorMessage Set to an error message if linking fails
+ *
+ *  \return True if linking succeeds otherwise false
+ */
+static bool linkBCA(object::Archive* archive, Module* composite, std::string& errorMessage)
+{
+  llvm::raw_string_ostream SS(errorMessage);
+  std::vector<Module*> archiveModules;
+
+  // Is this efficient? Could we use StringRef instead?
+  std::set<std::string> undefinedSymbols;
+  GetAllUndefinedSymbols(composite, undefinedSymbols);
+
+  if (undefinedSymbols.size() == 0)
+  {
+    // Nothing to do
+    DEBUG_WITH_TYPE("klee_linker", dbgs() << "No undefined symbols. Not linking anything in!\n");
+    return true;
+  }
+
+  DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading modules\n");
+  // Load all bitcode files in to memory so we can examine their symbols
+  for (object::Archive::child_iterator AI = archive->begin_children(),
+       AE = archive->end_children(); AI != AE; ++AI)
+  {
+
+    StringRef memberName;
+    error_code ec = AI->getName(memberName);
+
+    if ( ec == errc::success )
+    {
+      DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loading archive member " << memberName << "\n");
+    }
+    else
+    {
+      errorMessage="Archive member does not have a name!\n";
+      return false;
+    }
+
+    OwningPtr<object::Binary> child;
+    ec = AI->getAsBinary(child);
+    if (ec != object::object_error::success)
+    {
+      // If we can't open as a binary object file its hopefully a bitcode file
+
+      OwningPtr<MemoryBuffer> buff; // Once this is destroyed will Module still be valid??
+      Module *Result = 0;
+
+      if (error_code ec = AI->getMemoryBuffer(buff))
+      {
+        SS << "Failed to get MemoryBuffer: " <<ec.message();
+        SS.flush();
+        return false;
+      }
+
+      if (buff)
+      {
+        // FIXME: Maybe load bitcode file lazily? Then if we need to link, materialise the module
+        Result = ParseBitcodeFile(buff.get(), getGlobalContext(), &errorMessage);
+
+        if(!Result)
+        {
+          SS << "Loading module failed : " << errorMessage << "\n";
+          SS.flush();
+          return false;
+        }
+        archiveModules.push_back(Result);
+      }
+      else
+      {
+        errorMessage="Buffer was NULL!";
+        return false;
+      }
+
+    }
+    else if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(child.get()))
+    {
+      SS << "Object file " << o->getFileName().data() <<
+            " in archive is not supported";
+      SS.flush();
+      return false;
+    }
+    else
+    {
+      SS << "Loading archive child with error "<< ec.message();
+      SS.flush();
+      return false;
+    }
+
+  }
+
+  DEBUG_WITH_TYPE("klee_linker", dbgs() << "Loaded " << archiveModules.size() << " modules\n");
+
+
+  std::set<std::string> previouslyUndefinedSymbols;
+
+  // Walk through the modules looking for definitions of undefined symbols
+  // if we find a match we should link that module in.
+  unsigned int passCounter=0;
+  do
+  {
+    unsigned int modulesLoadedOnPass=0;
+    previouslyUndefinedSymbols = undefinedSymbols;
+
+    for (size_t i = 0, j = archiveModules.size(); i < j; ++i)
+    {
+      // skip empty archives
+      if (archiveModules[i] == 0)
+        continue;
+      Module * M = archiveModules[i];
+      // Look for the undefined symbols in the composite module
+      for (std::set<std::string>::iterator S = undefinedSymbols.begin(), SE = undefinedSymbols.end();
+         S != SE; ++S)
+      {
+
+        // FIXME: We aren't handling weak symbols here!
+        // However the algorithm used in LLVM3.2 didn't seem to either
+        // so maybe it doesn't matter?
+
+        if ( GlobalValue* GV = dyn_cast_or_null<GlobalValue>(M->getValueSymbolTable().lookup(*S)))
+        {
+          if (GV->isDeclaration()) continue; // Not a definition
+
+          DEBUG_WITH_TYPE("klee_linker", dbgs() << "Found " << GV->getName() <<
+              " in " << M->getModuleIdentifier() << "\n");
+
+
+          if (Linker::LinkModules(composite, M, Linker::DestroySource, &errorMessage))
+          {
+            // Linking failed
+            SS << "Linking archive module with composite failed:" << errorMessage;
+            SS.flush();
+            CleanUpLinkBCA(archiveModules);
+            return false;
+          }
+          else
+          {
+            // Link succeed, now clean up
+            modulesLoadedOnPass++;
+            DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking succeeded.\n");
+
+            delete M;
+            archiveModules[i] = 0;
+
+            // We need to recompute the undefined symbols in the composite module
+            // after linking
+            GetAllUndefinedSymbols(composite, undefinedSymbols);
+
+            break; // Look for symbols in next module
+          }
+
+        }
+      }
+    }
+
+    passCounter++;
+    DEBUG_WITH_TYPE("klee_linker", dbgs() << "Completed " << passCounter <<
+                " linker passes.\n" << modulesLoadedOnPass <<
+                " modules loaded on the last pass\n");
+  } while (undefinedSymbols != previouslyUndefinedSymbols); // Iterate until we reach a fixed point
+
+
+  // What's left in archiveModules we don't want to link in so free it
+  CleanUpLinkBCA(archiveModules);
+
+  return true;
+
+}
+#endif
+
+
 Module *klee::linkWithLibrary(Module *module, 
                               const std::string &libraryName) {
+DEBUG_WITH_TYPE("klee_linker", dbgs() << "Linking file " << libraryName << "\n");
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
-  SMDiagnostic err;
-  std::string err_str;
-  sys::Path libraryPath(libraryName);
-  Module *new_mod = ParseIRFile(libraryPath.str(), err, 
-module->getContext());
-
-  if (Linker::LinkModules(module, new_mod, Linker::DestroySource, 
-&err_str)) {
-    assert(0 && "linked in library failed!");
+  if (!sys::fs::exists(libraryName)) {
+    klee_error("Link with library %s failed. No such file.",
+        libraryName.c_str());
+  }
+
+  OwningPtr<MemoryBuffer> Buffer;
+  if (error_code ec = MemoryBuffer::getFile(libraryName,Buffer)) {
+    klee_error("Link with library %s failed: %s", libraryName.c_str(),
+        ec.message().c_str());
+  }
+
+  sys::fs::file_magic magic = sys::fs::identify_magic(Buffer->getBuffer());
+
+  LLVMContext &Context = getGlobalContext();
+  std::string ErrorMessage;
+
+  if (magic == sys::fs::file_magic::bitcode) {
+    Module *Result = 0;
+    Result = ParseBitcodeFile(Buffer.get(), Context, &ErrorMessage);
+
+
+    if (!Result || Linker::LinkModules(module, Result, Linker::DestroySource,
+        &ErrorMessage))
+      klee_error("Link with library %s failed: %s", libraryName.c_str(),
+          ErrorMessage.c_str());
+
+    delete Result;
+
+  } else if (magic == sys::fs::file_magic::archive) {
+    OwningPtr<object::Binary> arch;
+    if (error_code ec = object::createBinary(Buffer.take(), arch))
+      klee_error("Link with library %s failed: %s", libraryName.c_str(),
+          ec.message().c_str());
+
+    if (object::Archive *a = dyn_cast<object::Archive>(arch.get())) {
+      // Handle in helper
+      if (!linkBCA(a, module, ErrorMessage))
+        klee_error("Link with library %s failed: %s", libraryName.c_str(),
+            ErrorMessage.c_str());
+    }
+    else {
+    	klee_error("Link with library %s failed: Cast to archive failed", libraryName.c_str());
+    }
+
+  } else if (magic.is_object()) {
+    OwningPtr<object::Binary> obj;
+    if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(obj.get())) {
+      klee_warning("Link with library: Object file %s in archive %s found. "
+          "Currently not supported.",
+          o->getFileName().data(), libraryName.c_str());
+    }
+  } else {
+    klee_error("Link with library %s failed: Unrecognized file type.",
+        libraryName.c_str());
   }
 
   return module;
@@ -66,13 +410,15 @@ module->getContext());
   bool native = false;
     
   if (linker.LinkInFile(libraryPath, native)) {
-    assert(0 && "linking in library failed!");
+    klee_error("Linking library %s failed", libraryName.c_str());
   }
     
   return linker.releaseModule();
 #endif
 }
 
+
+
 Function *klee::getDirectCallTarget(CallSite cs) {
   Value *v = cs.getCalledValue();
   if (Function *f = dyn_cast<Function>(v)) {
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index 41a106f1..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
@@ -124,7 +123,9 @@ static void AddStandardCompilePasses(PassManager &PM) {
     addPass(PM, createFunctionInliningPass());   // Inline small functions
   addPass(PM, createArgumentPromotionPass());    // Scalarize uninlined fn args
 
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 4)
   addPass(PM, createSimplifyLibCallsPass());     // Library Call Optimizations
+#endif
   addPass(PM, createInstructionCombiningPass()); // Cleanup for scalarrepl.
   addPass(PM, createJumpThreadingPass());        // Thread jumps.
   addPass(PM, createCFGSimplificationPass());    // Merge & remove BBs
@@ -270,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 08a9ef7c..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;
 }
@@ -363,12 +366,12 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     return ConstantExpr::alloc((it == objects.end() ? 127 : 
                                 it->second->getPossibleValue(index)),
-                               Expr::Int8);
+                               array.getRange());
   }
 
 public:
@@ -384,19 +387,19 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     if (it == objects.end())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
     CexValueData cvd = it->second->getExactValues(index);
     if (!cvd.isFixed())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
-    return ConstantExpr::alloc(cvd.min(), Expr::Int8);
+    return ConstantExpr::alloc(cvd.min(), array.getRange());
   }
 
 public:
@@ -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;
@@ -1109,13 +1106,14 @@ FastCexSolver::computeInitialValues(const Query& query,
   // Propogation found a satisfying assignment, compute the initial values.
   for (unsigned i = 0; i != objects.size(); ++i) {
     const Array *array = objects[i];
+    assert(array);
     std::vector<unsigned char> data;
     data.reserve(array->size);
 
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
         ReadExpr::create(UpdateList(array, 0),
-                         ConstantExpr::create(i, Expr::Int32));
+                         ConstantExpr::create(i, array->getDomain()));
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
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/Makefile b/lib/Solver/Makefile
index 2be74c01..a44b4f6e 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -12,6 +12,7 @@ LEVEL=../..
 LIBRARYNAME=kleaverSolver
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
 
@@ -22,4 +23,4 @@ ifeq ($(ENABLE_METASMT),1)
   CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
   CXX.Flags += $(metaSMT_CXXFLAGS)
   CXX.Flags += $(metaSMT_INCLUDES)
-endif
\ No newline at end of file
+endif
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 2b084ac7..b5c99907 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -187,7 +187,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArr
 
     if (!hashed) {
 
-        array_expr = evaluate(_solver, buildArray(8, 32));	
+        array_expr = evaluate(_solver, buildArray(root->getRange(), root->getDomain()));
 
         if (root->isConstantArray()) {    
             for (unsigned i = 0, e = root->size; i != e; ++i) {
@@ -599,11 +599,11 @@ 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()) {    
+    switch (e->getKind()) {
 
         case Expr::Constant:
         {
@@ -614,7 +614,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 
             // Coerce to bool if necessary.
             if (coe_width == 1) {
-                res = (coe->isTrue()) ? getTrue() : getFalse();      
+                res = (coe->isTrue()) ? getTrue() : getFalse();
             }
             else if (coe_width <= 32) {
                  res = bvConst32(coe_width, coe->getZExtValue(32));
@@ -624,7 +624,7 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
             }
             else {
                  ref<ConstantExpr> tmp = coe;
-                 res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());                 
+                 res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue());
                  while (tmp->getWidth() > 64) {
                      tmp = tmp->Extract(64, tmp->getWidth() -  64);
                      unsigned min_width = std::min(64U, tmp->getWidth());
@@ -658,9 +658,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
         case Expr::Read:
         {
             ReadExpr *re = cast<ReadExpr>(e);
-            assert(re);
+            assert(re && re->updates.root);
+            *width_out = re->updates.root->getRange();
             // FixMe call method of Array
-            *width_out = 8;
             res = evaluate(_solver, 
                            metaSMT::logic::Array::select(
                                   getArrayForUpdate(re->updates.root, re->updates.head),
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 90252656..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>
@@ -174,14 +173,13 @@ ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) {
 }
 
 // logical right shift
-ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
+ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned shift) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width) {
-    return bvZero(width);
+    return bvZero(width); // Overshift to zero
   } else {
     return vc_bvConcatExpr(vc,
                            bvZero(shift),
@@ -190,14 +188,13 @@ ExprHandle STPBuilder::bvRightShift(ExprHandle expr, unsigned amount, unsigned s
 }
 
 // logical left shift
-ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned shiftBits) {
+ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width) {
-    return bvZero(width);
+    return bvZero(width); // Overshift to zero
   } else {
     // stp shift does "expr @ [0 x s]" which we then have to extract,
     // rolling our own gives slightly smaller exprs
@@ -208,96 +205,97 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned amount, unsigned sh
 }
 
 // left shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width) {
+ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
+  unsigned width = vc_getBVLength(vc, expr);
   ExprHandle res = bvZero(width);
 
-  int shiftBits = getShiftBits( width );
-
-  //get the shift amount (looking only at the bits appropriate for the given width)
-  ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); 
-
   //construct a big if-then-elif-elif-... with one case per possible shift amount
   for( int i=width-1; i>=0; i-- ) {
     res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(shiftBits, i)),
-                     bvLeftShift(expr, i, shiftBits),
+                     eqExpr(shift, bvConst32(width, i)),
+                     bvLeftShift(expr, i),
                      res);
   }
+
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 // logical right shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width) {
+ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
+  unsigned width = vc_getBVLength(vc, expr);
   ExprHandle res = bvZero(width);
 
-  int shiftBits = getShiftBits( width );
-
-  //get the shift amount (looking only at the bits appropriate for the given width)
-  ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 ); 
-
   //construct a big if-then-elif-elif-... with one case per possible shift amount
   for( int i=width-1; i>=0; i-- ) {
     res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(shiftBits, i)),
-                     bvRightShift(expr, i, shiftBits),
+                     eqExpr(shift, bvConst32(width, i)),
+                     bvRightShift(expr, i),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 // arithmetic right shift by a variable amount on an expression of the specified width
-ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width) {
-  int shiftBits = getShiftBits( width );
-
-  //get the shift amount (looking only at the bits appropriate for the given width)
-  ExprHandle shift = vc_bvExtract( vc, amount, shiftBits - 1, 0 );
+ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
+  unsigned width = vc_getBVLength(vc, expr);
 
   //get the sign bit to fill with
   ExprHandle signedBool = bvBoolExtract(expr, width-1);
 
   //start with the result if shifting by width-1
-  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool, shiftBits);
+  ExprHandle res = constructAShrByConstant(expr, width-1, signedBool);
 
   //construct a big if-then-elif-elif-... with one case per possible shift amount
   // XXX more efficient to move the ite on the sign outside all exprs?
   // XXX more efficient to sign extend, right shift, then extract lower bits?
   for( int i=width-2; i>=0; i-- ) {
     res = vc_iteExpr(vc,
-                     eqExpr(shift, bvConst32(shiftBits,i)),
+                     eqExpr(shift, bvConst32(width,i)),
                      constructAShrByConstant(expr, 
                                              i, 
-                                             signedBool, 
-                                             shiftBits),
+                                             signedBool),
                      res);
   }
 
+  // If overshifting, shift to zero
+  res = vc_iteExpr(vc,
+                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   res,
+                   bvZero(width));
   return res;
 }
 
 ExprHandle STPBuilder::constructAShrByConstant(ExprHandle expr,
-                                               unsigned amount,
-                                               ExprHandle isSigned, 
-                                               unsigned shiftBits) {
+                                               unsigned shift,
+                                               ExprHandle isSigned) {
   unsigned width = vc_getBVLength(vc, expr);
-  unsigned shift = amount & ((1<<shiftBits) - 1);
 
   if (shift==0) {
     return expr;
   } else if (shift>=width-1) {
-    return vc_iteExpr(vc, isSigned, bvMinusOne(width), bvZero(width));
+    return bvZero(width); // Overshift to zero
   } else {
     return vc_iteExpr(vc,
                       isSigned,
                       ExprHandle(vc_bvConcatExpr(vc,
                                                  bvMinusOne(shift),
                                                  bvExtract(expr, width - 1, shift))),
-                      bvRightShift(expr, shift, shiftBits));
+                      bvRightShift(expr, shift));
   }
 }
 
 ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x) {
-  unsigned shiftBits = getShiftBits(width);
   uint64_t add, sub;
   ExprHandle res = 0;
 
@@ -313,7 +311,7 @@ ExprHandle STPBuilder::constructMulByConstant(ExprHandle expr, unsigned width, u
 
     if ((add&bit) || (sub&bit)) {
       assert(!((add&bit) && (sub&bit)) && "invalid mult constants");
-      ExprHandle op = bvLeftShift(expr, j, shiftBits);
+      ExprHandle op = bvLeftShift(expr, j);
       
       if (add&bit) {
         if (res) {
@@ -367,9 +365,9 @@ ExprHandle STPBuilder::constructUDivByConstant(ExprHandle expr_n, unsigned width
 
   // n/d = (((n - t1) >> sh1) + t1) >> sh2;
   ExprHandle n_minus_t1  = vc_bvMinusExpr( vc, width, expr_n, t1 );
-  ExprHandle shift_sh1   = bvVarRightShift( n_minus_t1, expr_sh1, 32 );
+  ExprHandle shift_sh1   = bvVarRightShift( n_minus_t1, expr_sh1);
   ExprHandle plus_t1     = vc_bvPlusExpr( vc, width, shift_sh1, t1 );
-  ExprHandle res         = bvVarRightShift( plus_t1, expr_sh2, 32 );
+  ExprHandle res         = bvVarRightShift( plus_t1, expr_sh2);
 
   return res;
 }
@@ -407,7 +405,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
   // Improved variable arithmetic right shift: sign extend, shift,
   // extract.
   ExprHandle extend_npm   = vc_bvSignExtend( vc, n_plus_mulsh, 64 );
-  ExprHandle shift_npm    = bvVarRightShift( extend_npm, expr_shpost, 64 );
+  ExprHandle shift_npm    = bvVarRightShift( extend_npm, expr_shpost);
   ExprHandle shift_shpost = vc_bvExtract( vc, shift_npm, 31, 0 ); //lower 32-bits
 
   // XSIGN(n) is -1 if n is negative, positive one otherwise
@@ -440,7 +438,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
     memmove(buf + space, buf, addrlen); // moving the address part to the end
     memcpy(buf, root->name.c_str(), space); // filling out the name part
     
-    array_expr = buildArray(buf, 32, 8);
+    array_expr = buildArray(buf, root->getDomain(), root->getRange());
     
     if (root->isConstantArray()) {
       // FIXME: Flush the concrete values into STP. Ideally we would do this
@@ -554,7 +552,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   case Expr::Read: {
     ReadExpr *re = cast<ReadExpr>(e);
-    *width_out = 8;
+    assert(re && re->updates.root);
+    *width_out = re->updates.root->getRange();
     return vc_readExpr(vc,
                        getArrayForUpdate(re->updates.root, re->updates.head),
                        construct(re->index, 0));
@@ -659,8 +658,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
       
         if (bits64::isPowerOfTwo(divisor)) {
           return bvRightShift(left,
-                              bits64::indexOfSingleBit(divisor),
-                              getShiftBits(*width_out));
+                              bits64::indexOfSingleBit(divisor));
         } else if (optimizeDivides) {
           if (*width_out == 32) //only works for 32-bit division
             return constructUDivByConstant( left, *width_out, 
@@ -810,28 +808,25 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
-      return bvLeftShift(left, (unsigned) CE->getLimitedValue(), 
-                         getShiftBits(*width_out));
+      return bvLeftShift(left, (unsigned) CE->getLimitedValue());
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
-      return bvVarLeftShift( left, amount, *width_out );
+      return bvVarLeftShift( left, amount);
     }
   }
 
   case Expr::LShr: {
     LShrExpr *lse = cast<LShrExpr>(e);
     ExprHandle left = construct(lse->left, width_out);
-    unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
-      return bvRightShift(left, (unsigned) CE->getLimitedValue(), 
-                          shiftBits);
+      return bvRightShift(left, (unsigned) CE->getLimitedValue());
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
-      return bvVarRightShift( left, amount, *width_out );
+      return bvVarRightShift( left, amount);
     }
   }
 
@@ -843,12 +838,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
       unsigned shift = (unsigned) CE->getLimitedValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
-      return constructAShrByConstant(left, shift, signedBool, 
-                                     getShiftBits(*width_out));
+      return constructAShrByConstant(left, shift, signedBool);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(ase->right, &shiftWidth);
-      return bvVarArithRightShift( left, amount, *width_out );
+      return bvVarArithRightShift( left, amount);
     }
   }
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 0a99b753..ef1cd8b3 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -79,13 +79,6 @@ class STPBuilder {
   STPArrayExprHash _arr_hash;
 
 private:  
-  unsigned getShiftBits(unsigned amount) {
-    unsigned bits = 1;
-    amount--;
-    while (amount >>= 1)
-      bits++;
-    return bits;
-  }
 
   ExprHandle bvOne(unsigned width);
   ExprHandle bvZero(unsigned width);
@@ -100,14 +93,14 @@ private:
   ExprHandle eqExpr(ExprHandle a, ExprHandle b);
 
   //logical left and right shift (not arithmetic)
-  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift, unsigned shiftBits);
-  ExprHandle bvRightShift(ExprHandle expr, unsigned amount, unsigned shiftBits);
-  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle amount, unsigned width);
-  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
-  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle amount, unsigned width);
+  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
+  ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
+  ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
-                                     ExprHandle isSigned, unsigned shiftBits);
+                                     ExprHandle isSigned);
   ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x);
   ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
   ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 22b1545f..229fa234 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query,
     std::vector< ref<Expr> > bindings;
     for (unsigned i = 0; i != values.size(); ++i) {
       const Array *array = objects[i];
+      assert(array);
       for (unsigned j=0; j<array->size; j++) {
         unsigned char value = values[i][j];
         bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
-                                                           ConstantExpr::alloc(j, Expr::Int32)),
-                                          ConstantExpr::alloc(value, Expr::Int8)));
+                                                           ConstantExpr::alloc(j, array->getDomain())),
+                                          ConstantExpr::alloc(value, array->getRange())));
       }
     }
     ConstraintManager tmp(bindings);
@@ -493,8 +494,6 @@ Solver *klee::createDummySolver() {
 
 class STPSolverImpl : public SolverImpl {
 private:
-  /// The solver we are part of, for access to public information.
-  STPSolver *solver;
   VC vc;
   STPBuilder *builder;
   double timeout;
@@ -502,7 +501,7 @@ private:
   SolverRunStatus runStatusCode;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
+  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
   
   char *getConstraintLog(const Query&);
@@ -526,9 +525,8 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
-  : solver(_solver),
-    vc(vc_createValidityChecker()),
+STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+  : vc(vc_createValidityChecker()),
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP),
@@ -565,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() {
 /***/
 
 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
+  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
 {
 }
 
@@ -773,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/Makefile b/lib/Support/Makefile
index a1b46f3c..67272908 100644
--- a/lib/Support/Makefile
+++ b/lib/Support/Makefile
@@ -12,5 +12,6 @@ LEVEL=../..
 LIBRARYNAME=kleeSupport
 DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
+NO_INSTALL=1
 
 include $(LEVEL)/Makefile.common
diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp
new file mode 100644
index 00000000..676ce307
--- /dev/null
+++ b/lib/Support/MemoryUsage.cpp
@@ -0,0 +1,25 @@
+//===-- MemoryUsage.cpp ---------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Internal/System/MemoryUsage.h"
+#include <malloc.h>
+
+using namespace klee;
+
+size_t util::GetTotalMallocUsage() {
+  struct mallinfo mi = ::mallinfo();
+  // The malloc implementation in glibc (pmalloc2)
+  // does not include mmap()'ed memory in mi.uordblks
+  // but other implementations (e.g. tcmalloc) do.
+#if defined(__GLIBC__)
+  return mi.uordblks + mi.hblkhd;
+#else
+  return mi.uordblks;
+#endif
+}
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;