26 files changed, 2035 insertions, 60 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index ac0474fb..eac54141 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,5 +73,22 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     llvm::cl::CommaSeparated
 );
 
+#ifdef SUPPORT_METASMT
+
+llvm::cl::opt<klee::MetaSMTBackendType>
+UseMetaSMT("use-metasmt",
+           llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."),
+           llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"),
+                      clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
+                      clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
+                      clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"),
+                      clEnumValEnd),  
+           llvm::cl::init(METASMT_BACKEND_NONE));
+
+#endif /* SUPPORT_METASMT */
+
 }
 
+
+
+
diff --git a/lib/Core/CallPathManager.cpp b/lib/Core/CallPathManager.cpp
index ca127f25..03e75108 100644
--- a/lib/Core/CallPathManager.cpp
+++ b/lib/Core/CallPathManager.cpp
@@ -13,7 +13,12 @@
 
 #include <map>
 #include <vector>
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
+
 #include "llvm/Support/raw_ostream.h"
 
 using namespace llvm;
diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp
index 979970aa..935e4316 100644
--- a/lib/Core/Context.cpp
+++ b/lib/Core/Context.cpp
@@ -11,8 +11,13 @@
 
 #include "klee/Expr.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Type.h"
+#include "llvm/IR/DerivedTypes.h"
+#else
 #include "llvm/Type.h"
 #include "llvm/DerivedTypes.h"
+#endif
 
 #include <cassert>
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index db685639..b2c2a737 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -17,8 +17,11 @@
 #include "klee/Expr.h"
 
 #include "Memory.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
 #include "llvm/Support/CommandLine.h"
 
 #include <iostream>
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 069022a2..b2cff8ba 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -47,6 +47,19 @@
 #include "klee/Internal/Support/FloatEvaluation.h"
 #include "klee/Internal/System/Time.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Attributes.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/DataLayout.h"
+#include "llvm/IR/TypeBuilder.h"
+#else
 #include "llvm/Attributes.h"
 #include "llvm/BasicBlock.h"
 #include "llvm/Constants.h"
@@ -57,6 +70,13 @@
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
+#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
+#include "llvm/Target/TargetData.h"
+#else
+#include "llvm/DataLayout.h"
+#include "llvm/TypeBuilder.h"
+#endif
+#endif
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CallSite.h"
@@ -67,11 +87,6 @@
 #else
 #include "llvm/Support/Process.h"
 #endif
-#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
-#include "llvm/Target/TargetData.h"
-#else
-#include "llvm/DataLayout.h"
-#endif
 
 #include <cassert>
 #include <algorithm>
@@ -90,6 +105,33 @@
 using namespace llvm;
 using namespace klee;
 
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+#endif /* SUPPORT_METASMT */
+
+
+
 namespace {
   cl::opt<bool>
   DumpStatesOnHalt("dump-states-on-halt",
@@ -253,7 +295,41 @@ Executor::Executor(const InterpreterOptions &opts,
       : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
       
   if (coreSolverTimeout) UseForkedCoreSolver = true;
-  Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);  
+  
+  Solver *coreSolver = NULL;
+  
+#ifdef SUPPORT_METASMT
+  if (UseMetaSMT != METASMT_BACKEND_NONE) {
+    
+    std::string backend;
+    
+    switch (UseMetaSMT) {
+          case METASMT_BACKEND_STP:
+              backend = "STP"; 
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_Z3:
+              backend = "Z3";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_BOOLECTOR:
+              backend = "Boolector";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          default:
+              assert(false);
+              break;
+    };
+    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  }
+  else {
+    coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+  }
+#else
+  coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+#endif /* SUPPORT_METASMT */
+  
+   
   Solver *solver = 
     constructSolverChain(coreSolver,
                          interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
@@ -386,10 +462,10 @@ void Executor::initializeGlobals(ExecutionState &state) {
 
   if (m->getModuleInlineAsm() != "")
     klee_warning("executable has module level assembly (ignoring)");
-
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   assert(m->lib_begin() == m->lib_end() &&
          "XXX do not support dependent libraries");
-
+#endif
   // represent function globals using the address of the actual llvm function
   // object. given that we use malloc to allocate memory in states this also
   // ensures that we won't conflict. we don't need to allocate a memory object
@@ -557,20 +633,31 @@ void Executor::branch(ExecutionState &state,
   unsigned N = conditions.size();
   assert(N);
 
-  stats::forks += N-1;
+  if (MaxForks!=~0u && stats::forks >= MaxForks) {
+    unsigned next = theRNG.getInt32() % N;
+    for (unsigned i=0; i<N; ++i) {
+      if (i == next) {
+        result.push_back(&state);
+      } else {
+        result.push_back(NULL);
+      }
+    }
+  } else {
+    stats::forks += N-1;
 
-  // XXX do proper balance or keep random?
-  result.push_back(&state);
-  for (unsigned i=1; i<N; ++i) {
-    ExecutionState *es = result[theRNG.getInt32() % i];
-    ExecutionState *ns = es->branch();
-    addedStates.insert(ns);
-    result.push_back(ns);
-    es->ptreeNode->data = 0;
-    std::pair<PTree::Node*,PTree::Node*> res = 
-      processTree->split(es->ptreeNode, ns, es);
-    ns->ptreeNode = res.first;
-    es->ptreeNode = res.second;
+    // XXX do proper balance or keep random?
+    result.push_back(&state);
+    for (unsigned i=1; i<N; ++i) {
+      ExecutionState *es = result[theRNG.getInt32() % i];
+      ExecutionState *ns = es->branch();
+      addedStates.insert(ns);
+      result.push_back(ns);
+      es->ptreeNode->data = 0;
+      std::pair<PTree::Node*,PTree::Node*> res = 
+        processTree->split(es->ptreeNode, ns, es);
+      ns->ptreeNode = res.first;
+      es->ptreeNode = res.second;
+    }
   }
 
   // If necessary redistribute seeds to match conditions, killing
@@ -605,12 +692,14 @@ void Executor::branch(ExecutionState &state,
       if (i==N)
         i = theRNG.getInt32() % N;
 
-      seedMap[result[i]].push_back(*siit);
+      // Extra check in case we're replaying seeds with a max-fork
+      if (result[i])
+        seedMap[result[i]].push_back(*siit);
     }
 
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
-        if (!seedMap.count(result[i])) {
+        if (result[i] && !seedMap.count(result[i])) {
           terminateState(*result[i]);
           result[i] = NULL;
         }
@@ -1380,7 +1469,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                            CallSite(cast<CallInst>(caller)));
 
             // XXX need to check other param attrs ?
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+      bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
 	    bool isSExt = cs.paramHasAttr(0, llvm::Attributes::SExt);
 #else
 	    bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt);
@@ -1584,7 +1675,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
             if (from != to) {
               // XXX need to check other param attrs ?
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+              bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
 	      bool isSExt = cs.paramHasAttr(i+1, llvm::Attributes::SExt);
 #else
 	      bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt);
@@ -1982,8 +2075,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FAdd operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -1996,9 +2094,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(left->getWidth()) ||
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FSub operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2012,8 +2114,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FMul operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2027,8 +2134,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FDiv operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2041,9 +2153,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(left->getWidth()) ||
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FRem operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.remainder(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()));
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2056,7 +2172,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth())
       return terminateStateOnExecError(state, "Unsupported FPTrunc operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Res(arg->getAPValue());
+#endif
     bool losesInfo = false;
     Res.convert(*fpWidthToSemantics(resultType),
                 llvm::APFloat::rmNearestTiesToEven,
@@ -2072,8 +2192,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                         "floating point");
     if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType)
       return terminateStateOnExecError(state, "Unsupported FPExt operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Res(arg->getAPValue());
+#endif
     bool losesInfo = false;
     Res.convert(*fpWidthToSemantics(resultType),
                 llvm::APFloat::rmNearestTiesToEven,
@@ -2090,7 +2213,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
       return terminateStateOnExecError(state, "Unsupported FPToUI operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Arg(arg->getAPValue());
+#endif
     uint64_t value = 0;
     bool isExact = true;
     Arg.convertToInteger(&value, resultType, false,
@@ -2106,8 +2233,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                        "floating point");
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
       return terminateStateOnExecError(state, "Unsupported FPToSI operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Arg(arg->getAPValue());
+
+#endif
     uint64_t value = 0;
     bool isExact = true;
     Arg.convertToInteger(&value, resultType, true,
@@ -2158,8 +2289,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FCmp operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue());
+    APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue());
+#else
     APFloat LHS(left->getAPValue());
     APFloat RHS(right->getAPValue());
+#endif
     APFloat::cmpResult CmpRes = LHS.compare(RHS);
 
     bool Result = false;
@@ -2470,8 +2606,11 @@ 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
         if (mbs > MaxMemory) {
           if (mbs > MaxMemory + 100) {
             // just guess at how many to kill
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 2fda5cba..6a5314ca 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -20,7 +20,12 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/System/Time.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
+
 #include "llvm/Support/CommandLine.h"
 
 #include <unistd.h>
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 0d85afee..9e83b32c 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -20,6 +20,13 @@
 
 #include "klee/util/GetElementPtrTypeIterator.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/DataLayout.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
@@ -27,12 +34,16 @@
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
 #include "llvm/ModuleProvider.h"
 #endif
-#include "llvm/Support/CallSite.h"
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
 #include "llvm/Target/TargetData.h"
 #else
 #include "llvm/DataLayout.h"
 #endif
+#endif
+
+#include "llvm/Support/CallSite.h"
+
+
 #include <iostream>
 #include <cassert>
 
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 7da0c350..344811d4 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -17,6 +17,13 @@
 #undef PACKAGE_TARNAME
 #undef PACKAGE_VERSION
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/LLVMContext.h"
+#else
 #include "llvm/Module.h"
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
@@ -27,6 +34,7 @@
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
+#endif
 #include "llvm/ExecutionEngine/JIT.h"
 #include "llvm/ExecutionEngine/GenericValue.h"
 #include "llvm/Support/CallSite.h"
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 08c95d48..4bcdd9f7 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -19,9 +19,16 @@
 #include "ObjectHolder.h"
 #include "MemoryManager.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include <llvm/IR/Function.h>
+#include <llvm/IR/Instruction.h>
+#include <llvm/IR/Value.h>
+#else
 #include <llvm/Function.h>
 #include <llvm/Instruction.h>
 #include <llvm/Value.h>
+#endif
+
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 778ef0ef..2dbabd01 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -25,10 +25,15 @@
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
+#endif
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index d44e13b6..04f32780 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -21,7 +21,11 @@
 #include "Executor.h"
 #include "MemoryManager.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Module.h"
+#endif
 #include "llvm/ADT/Twine.h"
 
 #include <errno.h>
@@ -131,7 +135,9 @@ void SpecialFunctionHandler::prepare() {
       // Make sure NoReturn attribute is set, for optimization and
       // coverage counting.
       if (hi.doesNotReturn)
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+        f->addFnAttr(Attribute::NoReturn);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
         f->addFnAttr(Attributes::NoReturn);
 #else
         f->addFnAttr(Attribute::NoReturn);
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index c0028a05..b5f38b2e 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -27,6 +27,15 @@
 #include "UserSearcher.h"
 #include "../Solver/SolverStats.h"
 
+#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/InlineAsm.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Type.h"
+#else
 #include "llvm/BasicBlock.h"
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
@@ -34,8 +43,10 @@
 #include "llvm/InlineAsm.h"
 #include "llvm/Module.h"
 #include "llvm/Type.h"
+#endif
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/CFG.h"
+#include "llvm/Support/raw_os_ostream.h"
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
 #include "llvm/System/Process.h"
 #else
@@ -401,7 +412,11 @@ void StatsTracker::writeStatsLine() {
              << "," << numBranches
              << "," << util::getUserTime()
              << "," << executor.states.size()
+#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
+             << "," << sys::Process::GetMallocUsage()
+#else
              << "," << sys::Process::GetTotalMemoryUsage()
+#endif
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index b759daae..90d9bcd4 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -11,6 +11,13 @@
 
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
+#include "llvm/Function.h"
+#endif
+#include "llvm/Support/CommandLine.h"
+#include "klee/Internal/Module/KModule.h"
 
 #include <iostream>
 #include <map>
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 67ed9aa7..c6fc9d3a 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -11,6 +11,19 @@
 
 #include "klee/Config/Version.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/InstrTypes.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Type.h"
+#include "llvm/IR/DataLayout.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Function.h"
@@ -18,19 +31,24 @@
 #include "llvm/Instruction.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
+#include "llvm/Module.h"
+#include "llvm/Type.h"
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
-#include "llvm/Module.h"
-#include "llvm/Pass.h"
-#include "llvm/Type.h"
-#include "llvm/Transforms/Scalar.h"
-#include "llvm/Transforms/Utils/BasicBlockUtils.h"
+
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
 #include "llvm/Target/TargetData.h"
 #else
 #include "llvm/DataLayout.h"
 #endif
+#endif
+#include "llvm/Pass.h"
+#include "llvm/Transforms/Scalar.h"
+#include "llvm/Transforms/Utils/BasicBlockUtils.h"
+#include "llvm/Support/CallSite.h"
+#include <iostream>
 
 using namespace llvm;
 using namespace klee;
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index d0ef52d0..9d4053d4 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -10,11 +10,18 @@
 #include "klee/Internal/Module/InstructionInfoTable.h"
 #include "klee/Config/Version.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#include "llvm/Linker.h"
 #include "llvm/Module.h"
+#endif
+#include "llvm/Linker.h"
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
 #include "llvm/Assembly/AsmAnnotationWriter.h"
 #else
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 2f18c17e..56d06d30 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -10,6 +10,19 @@
 #include "Passes.h"
 
 #include "klee/Config/Version.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/InstrTypes.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Type.h"
+#include "llvm/IR/IRBuilder.h"
+
+#else
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Function.h"
@@ -21,20 +34,21 @@
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
-#include "llvm/Pass.h"
 #include "llvm/Type.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
 #include "llvm/IRBuilder.h"
 #else
 #include "llvm/Support/IRBuilder.h"
 #endif
-#include "llvm/Transforms/Scalar.h"
-#include "llvm/Transforms/Utils/BasicBlockUtils.h"
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
 #include "llvm/Target/TargetData.h"
 #else
 #include "llvm/DataLayout.h"
 #endif
+#endif
+#include "llvm/Pass.h"
+#include "llvm/Transforms/Scalar.h"
+#include "llvm/Transforms/Utils/BasicBlockUtils.h"
 
 using namespace llvm;
 
@@ -46,11 +60,13 @@ bool IntrinsicCleanerPass::runOnModule(Module &M) {
   bool dirty = false;
   for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f)
     for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b)
-      dirty |= runOnBasicBlock(*b);
+      dirty |= runOnBasicBlock(*b, M);
+    if (Function *Declare = M.getFunction("llvm.trap"))
+      Declare->eraseFromParent();
   return dirty;
 }
 
-bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { 
+bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
   bool dirty = false;
   
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
@@ -181,6 +197,24 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         ii->eraseFromParent();
         dirty = true;
         break;
+
+      case Intrinsic::trap: {
+        // Intrisic instruction "llvm.trap" found. Directly lower it to
+        // a call of the abort() function.
+        Function *F = cast<Function>(
+          M.getOrInsertFunction(
+            "abort", Type::getVoidTy(getGlobalContext()), NULL));
+        F->setDoesNotReturn();
+        F->setDoesNotThrow();
+
+        CallInst::Create(F, Twine(), ii);
+        new UnreachableInst(getGlobalContext(), ii);
+
+        ii->eraseFromParent();
+
+        dirty = true;
+        break;
+      }
                     
       default:
         if (LowerIntrinsics)
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index b646ca6e..ff13efda 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -22,13 +22,28 @@
 #include "klee/Internal/Support/ModuleUtil.h"
 
 #include "llvm/Bitcode/ReaderWriter.h"
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/ValueSymbolTable.h"
+#include "llvm/IR/DataLayout.h"
+#else
 #include "llvm/Instructions.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/Module.h"
-#include "llvm/PassManager.h"
 #include "llvm/ValueSymbolTable.h"
+#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
+#include "llvm/Target/TargetData.h"
+#else
+#include "llvm/DataLayout.h"
+#endif
+
+#endif
+
+#include "llvm/PassManager.h"
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
@@ -40,11 +55,6 @@
 #else
 #include "llvm/Support/Path.h"
 #endif
-#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
-#include "llvm/Target/TargetData.h"
-#else
-#include "llvm/DataLayout.h"
-#endif
 #include "llvm/Transforms/Scalar.h"
 
 #include <llvm/Transforms/Utils/Cloning.h>
@@ -193,6 +203,7 @@ static void injectStaticConstructorsAndDestructors(Module *m) {
   }
 }
 
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
 static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType,
                         ...) {
   // If module lacks an externally visible symbol for the name then we
@@ -215,6 +226,7 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType,
     m->getOrInsertFunction(name, FunctionType::get(retType, argTypes, false));
   }
 }
+#endif
 
 /// This function will take try to inline all calls to \p functionName
 /// in the module \p module .
@@ -332,7 +344,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
 
   if (opts.Optimize)
     Optimize(module);
-
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   // Force importing functions required by intrinsic lowering. Kind of
   // unfortunate clutter when we don't need them but we won't know
   // that until after all linking and intrinsic lowering is
@@ -353,14 +365,18 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
               PointerType::getUnqual(i8Ty),
               Type::getInt32Ty(getGlobalContext()),
               targetData->getIntPtrType(getGlobalContext()), (Type*) 0);
-
+#endif
   // FIXME: Missing force import for various math functions.
 
   // 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");
+#else
   path.appendComponent("libkleeRuntimeIntrinsic.bca");
+#endif
   module = linkWithLibrary(module, path.c_str());
 
   /* In order for KLEE to report ALL errors at instrumented
@@ -396,7 +412,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   pm3.add(new IntrinsicCleanerPass(*targetData));
   pm3.add(new PhiCleanerPass());
   pm3.run(*module);
-
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   // For cleanliness see if we can discard any of the functions we
   // forced to import.
   Function *f;
@@ -406,7 +422,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   if (f && f->use_empty()) f->eraseFromParent();
   f = module->getFunction("memset");
   if (f && f->use_empty()) f->eraseFromParent();
-
+#endif
 
   // Write out the .ll assembly file. We truncate long lines to work
   // around a kcachegrind parsing bug (it puts them on new lines), so
diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp
index e5382c1a..e1a5d5b2 100644
--- a/lib/Module/LowerSwitch.cpp
+++ b/lib/Module/LowerSwitch.cpp
@@ -16,7 +16,9 @@
 
 #include "Passes.h"
 #include "klee/Config/Version.h"
-#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/LLVMContext.h"
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include <algorithm>
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 029540ae..43eef0b7 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -10,11 +10,23 @@
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Config/Version.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/Bitcode/ReaderWriter.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IRReader/IRReader.h"
+#include "llvm/IR/Module.h"
+#include "llvm/Support/SourceMgr.h"
+#include "llvm/Support/DataStream.h"
+#else
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#include "llvm/Linker.h"
 #include "llvm/Module.h"
+#endif
+
+#include "llvm/Linker.h"
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
 #include "llvm/Assembly/AsmAnnotationWriter.h"
 #else
@@ -42,6 +54,20 @@ using namespace klee;
 
 Module *klee::linkWithLibrary(Module *module, 
                               const std::string &libraryName) {
+#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!");
+  }
+
+  return module;
+#else
   Linker linker("klee", module, false);
 
   llvm::sys::Path libraryPath(libraryName);
@@ -52,6 +78,7 @@ Module *klee::linkWithLibrary(Module *module,
   }
     
   return linker.releaseModule();
+#endif
 }
 
 Function *klee::getDirectCallTarget(CallSite cs) {
diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp
index 6da9a2c1..83ee93ee 100644
--- a/lib/Module/Optimize.cpp
+++ b/lib/Module/Optimize.cpp
@@ -16,7 +16,6 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/Config/Version.h"
-#include "llvm/Module.h"
 #include "llvm/PassManager.h"
 #include "llvm/Analysis/Passes.h"
 #include "llvm/Analysis/LoopPass.h"
@@ -27,11 +26,19 @@
 #else
 #include "llvm/Support/DynamicLibrary.h"
 #endif
+
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Module.h"
+#include "llvm/IR/DataLayout.h"
+#else
+#include "llvm/Module.h"
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
 #include "llvm/Target/TargetData.h"
 #else
 #include "llvm/DataLayout.h"
 #endif
+#endif
+
 #include "llvm/Target/TargetMachine.h"
 #include "llvm/Transforms/IPO.h"
 #include "llvm/Transforms/Scalar.h"
diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h
index b0d4c363..0c294daa 100644
--- a/lib/Module/Passes.h
+++ b/lib/Module/Passes.h
@@ -12,9 +12,15 @@
 
 #include "klee/Config/Version.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
+#endif
 #include "llvm/Pass.h"
 #include "llvm/CodeGen/IntrinsicLowering.h"
 
@@ -76,7 +82,7 @@ class IntrinsicCleanerPass : public llvm::ModulePass {
   llvm::IntrinsicLowering *IL;
   bool LowerIntrinsics;
 
-  bool runOnBasicBlock(llvm::BasicBlock &b);
+  bool runOnBasicBlock(llvm::BasicBlock &b, llvm::Module &M);
 public:
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
   IntrinsicCleanerPass(const llvm::TargetData &TD,
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index b5526f35..f15273e4 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -9,11 +9,16 @@
 
 #include "Passes.h"
 #include "klee/Config/Version.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/InlineAsm.h"
+#include "llvm/IR/LLVMContext.h"
+#else
 #include "llvm/InlineAsm.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
+#endif
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9)
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/Host.h"
diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile
index 11d3d330..2be74c01 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -14,3 +14,12 @@ DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
 
 include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_METASMT),1)
+  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
+  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
+  CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
+  CXX.Flags += $(metaSMT_CXXFLAGS)
+  CXX.Flags += $(metaSMT_INCLUDES)
+endif
\ No newline at end of file
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
new file mode 100644
index 00000000..2b084ac7
--- /dev/null
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -0,0 +1,1167 @@
+ /*
+ * MetaSMTBuilder.h
+ *
+ *  Created on: 8 Aug 2012
+ *      Author: hpalikar
+ */
+
+#ifndef METASMTBUILDER_H_
+#define METASMTBUILDER_H_
+
+#include "klee/Config/config.h"
+#include "klee/Expr.h"
+#include "klee/util/ExprPPrinter.h"
+#include "klee/util/ArrayExprHash.h"
+#include "klee/util/ExprHashMap.h"
+#include "ConstantDivision.h"
+
+#ifdef SUPPORT_METASMT
+
+#include "llvm/Support/CommandLine.h"
+
+#include <metaSMT/frontend/Logic.hpp>
+#include <metaSMT/frontend/QF_BV.hpp>
+#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/support/default_visitation_unrolling_limit.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+
+#define Expr VCExpr
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef STP
+ 
+#include <boost/mpl/vector.hpp>
+#include <boost/format.hpp>
+
+using namespace metaSMT;
+using namespace metaSMT::logic::QF_BV;
+
+
+#define DIRECT_CONTEXT
+
+namespace {
+  llvm::cl::opt<bool>
+  UseConstructHashMetaSMT("use-construct-hash-metasmt", 
+                   llvm::cl::desc("Use hash-consing during metaSMT query construction."),
+                   llvm::cl::init(true));
+}
+
+
+namespace klee {
+
+typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type  > const MetaSMTConstTrue;
+typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type  > const MetaSMTConstFalse;
+typedef metaSMT::logic::Array::array MetaSMTArray;
+
+template<typename SolverContext>
+class MetaSMTBuilder;
+
+template<typename SolverContext>
+class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > {
+    
+    friend class MetaSMTBuilder<SolverContext>;
+    
+public:
+    MetaSMTArrayExprHash() {};
+    virtual ~MetaSMTArrayExprHash() {};
+};
+
+static const bool mimic_stp = true;
+
+
+template<typename SolverContext>
+class MetaSMTBuilder {
+public:
+
+    MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { };
+    virtual ~MetaSMTBuilder() {};
+    
+    typename SolverContext::result_type construct(ref<Expr> e);
+    
+    typename SolverContext::result_type getInitialRead(const Array *root, unsigned index);
+    
+    typename SolverContext::result_type getTrue() {
+        return(evaluate(_solver, metaSMT::logic::True));        
+    }
+    
+    typename SolverContext::result_type getFalse() {        
+        return(evaluate(_solver, metaSMT::logic::False));        
+    }
+    
+    typename SolverContext::result_type bvOne(unsigned width) {
+        return bvZExtConst(width, 1);
+    }
+    
+    typename SolverContext::result_type bvZero(unsigned width) {
+        return bvZExtConst(width, 0);
+    }
+    
+    typename SolverContext::result_type bvMinusOne(unsigned width) {
+        return bvSExtConst(width, (int64_t) -1);
+    }
+    
+    typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) {
+        return(evaluate(_solver, bvuint(value, width)));
+    }
+    
+    typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) {
+         return(evaluate(_solver, bvuint(value, width)));
+    }
+       
+    typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value);    
+    typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value);
+    
+    //logical left and right shift (not arithmetic)
+    typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits);
+    typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits);
+    typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
+    typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
+    typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width);
+    
+    
+    typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un);
+    typename SolverContext::result_type getInitialArray(const Array *root);
+    MetaSMTArray buildArray(unsigned elem_width, unsigned index_width);
+        
+private:
+    typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> >  MetaSMTExprHashMap;
+    typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter;
+    typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter;    
+
+    SolverContext&  _solver;
+    bool _optimizeDivides;
+    MetaSMTArrayExprHash<SolverContext>  _arr_hash;
+    MetaSMTExprHashMap                   _constructed;
+    
+    typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out);
+    typename SolverContext::result_type construct(ref<Expr> e, int *width_out);
+    
+    typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit);
+    typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom);
+    typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b);
+    
+    typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, 
+                                                                typename SolverContext::result_type isSigned, unsigned shiftBits);
+    typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x);
+    typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
+    typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d);
+    
+    unsigned getShiftBits(unsigned amount) {
+        unsigned bits = 1;
+        amount--;
+        while (amount >>= 1) {
+            bits++;
+        }
+        return(bits);
+    }
+};
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) {
+  
+    if (!un) {
+        return(getInitialArray(root));
+    }
+    else {
+        typename SolverContext::result_type un_expr;
+        bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
+
+        if (!hashed) {
+            un_expr = evaluate(_solver,
+                               metaSMT::logic::Array::store(getArrayForUpdate(root, un->next),
+                                                            construct(un->index, 0),
+                                                            construct(un->value, 0)));
+            _arr_hash.hashUpdateNodeExpr(un, un_expr);
+        }
+        return(un_expr);
+    }
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root)
+{
+    assert(root);
+    typename SolverContext::result_type array_expr;
+    bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
+
+    if (!hashed) {
+
+        array_expr = evaluate(_solver, buildArray(8, 32));	
+
+        if (root->isConstantArray()) {    
+            for (unsigned i = 0, e = root->size; i != e; ++i) {
+                 typename SolverContext::result_type tmp =
+                            evaluate(_solver, 
+                                     metaSMT::logic::Array::store(array_expr,
+                                                                  construct(ConstantExpr::alloc(i, root->getDomain()), 0),
+                                                                  construct(root->constantValues[i], 0)));
+                array_expr = tmp;
+            }
+        }
+        _arr_hash.hashArrayExpr(root, array_expr);
+    }
+
+    return(array_expr);
+}
+
+template<typename SolverContext>
+MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) {
+    return(metaSMT::logic::Array::new_array(elem_width, index_width));
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) {
+    assert(root); 
+    assert(false);
+    typename SolverContext::result_type array_exp = getInitialArray(root);
+    typename SolverContext::result_type res = evaluate(
+                        _solver,
+                        metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain())));    
+    return(res);
+}
+
+
+template<typename SolverContext>  
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) {
+
+    typename SolverContext::result_type res;
+
+    if (width <= 64) {
+        res = bvConst64(width, value);
+    }
+    else {
+        typename SolverContext::result_type expr = bvConst64(64, value);
+        typename SolverContext::result_type zero = bvConst64(64, 0);
+
+        for (width -= 64; width > 64; width -= 64) {
+             expr = evaluate(_solver, concat(zero, expr));  
+        }
+        res = evaluate(_solver, concat(bvConst64(width, 0), expr));  
+    }
+
+    return(res); 
+}
+
+template<typename SolverContext>  
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) {
+  
+  typename SolverContext::result_type res;
+  
+  if (width <= 64) {
+      res = bvConst64(width, value); 
+  }
+  else {            
+      // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
+      res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value)));		     
+  }
+  return(res); 
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) {
+    return(evaluate(_solver,
+                    metaSMT::logic::equal(extract(bit, bit, expr),
+                                          bvOne(1))));
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) {    
+    return(evaluate(_solver, extract(top, bottom, expr)));
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) {    
+    return(evaluate(_solver, metaSMT::logic::equal(a, b)));
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount,
+                                                                                           typename SolverContext::result_type isSigned, unsigned shiftBits) {
+    unsigned shift = amount & ((1 << shiftBits) - 1);
+    typename SolverContext::result_type res;
+    
+    if (shift == 0) {
+        res = expr;
+    }
+    else if (shift >= width - 1) {
+        res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width)));
+    }
+    else {
+        res = evaluate(_solver, metaSMT::logic::Ite(isSigned,
+                                                    concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)),
+                                                    bvRightShift(expr, width, shift, shiftBits)));
+    }
+    
+    return(res);
+}
+
+// width is the width of expr; x -- number of bits to shift with
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) {
+    
+    unsigned shiftBits = getShiftBits(width);
+    uint64_t add, sub;
+    typename SolverContext::result_type res;
+    bool first = true;
+
+    // expr*x == expr*(add-sub) == expr*add - expr*sub
+    ComputeMultConstants64(x, add, sub);
+
+    // legal, these would overflow completely
+    add = bits64::truncateToNBits(add, width);
+    sub = bits64::truncateToNBits(sub, width);
+    
+    for (int j = 63; j >= 0; j--) {
+        uint64_t bit = 1LL << j;
+
+        if ((add & bit) || (sub & bit)) {
+            assert(!((add & bit) && (sub & bit)) && "invalid mult constants");
+
+            typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits);
+
+            if (add & bit) {
+                if (!first) {
+                    res = evaluate(_solver, bvadd(res, op));
+                } else {
+                    res = op;
+                    first = false;
+                }
+            } else {
+                if (!first) {
+                    res = evaluate(_solver, bvsub(res, op));                    
+                } else {
+                     // To reconsider: vc_bvUMinusExpr in STP
+                    res = evaluate(_solver, bvsub(bvZero(width), op));
+                    first = false;
+                }
+            }
+        }
+    }
+  
+    if (first) { 
+        res = bvZero(width);
+    }
+
+    return(res);
+}
+
+
+/* 
+ * Compute the 32-bit unsigned integer division of n by a divisor d based on 
+ * the constants derived from the constant divisor d.
+ *
+ * Returns n/d without doing explicit division.  The cost is 2 adds, 3 shifts, 
+ * and a (64-bit) multiply.
+ *
+ * @param expr_n numerator (dividend) n as an expression
+ * @param width  number of bits used to represent the value
+ * @param d      the divisor
+ *
+ * @return n/d without doing explicit division
+ */
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
+    
+    assert(width == 32 && "can only compute udiv constants for 32-bit division");
+    
+    // Compute the constants needed to compute n/d for constant d without division by d.
+    uint32_t mprime, sh1, sh2;
+    ComputeUDivConstants32(d, mprime, sh1, sh2);
+    typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1);
+    typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2);
+    
+    // t1  = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32
+    typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits
+    typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime);
+    typename SolverContext::result_type t1        = bvExtract(t1_64bits, 63, 32); //upper 32 bits
+    
+    // n/d = (((n - t1) >> sh1) + t1) >> sh2;
+    typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1));   
+    typename SolverContext::result_type shift_sh1  = bvVarRightShift(n_minus_t1, expr_sh1, 32);
+    typename SolverContext::result_type plus_t1    = evaluate(_solver, bvadd(shift_sh1, t1));    
+    typename SolverContext::result_type res        = bvVarRightShift(plus_t1, expr_sh2, 32);
+    
+    return(res);
+}
+
+/* 
+ * Compute the 32-bitnsigned integer division of n by a divisor d based on 
+ * the constants derived from the constant divisor d.
+ *
+ * Returns n/d without doing explicit division.  The cost is 3 adds, 3 shifts, 
+ * a (64-bit) multiply, and an XOR.
+ *
+ * @param n      numerator (dividend) as an expression
+ * @param width  number of bits used to represent the value
+ * @param d      the divisor
+ *
+ * @return n/d without doing explicit division
+ */
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) {
+    
+    assert(width == 32 && "can only compute udiv constants for 32-bit division");
+
+    // Compute the constants needed to compute n/d for constant d w/o division by d.
+    int32_t mprime, dsign, shpost;
+    ComputeSDivConstants32(d, mprime, dsign, shpost);
+    typename SolverContext::result_type expr_dsign  = bvConst32(32, dsign);
+    typename SolverContext::result_type expr_shpost = bvConst32(32, shpost);
+    
+    // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
+    int64_t mprime_64     = (int64_t)mprime;
+    
+    // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments
+    typename SolverContext::result_type expr_n_64    = evaluate(_solver, sign_extend(64 - width, expr_n));    
+    typename SolverContext::result_type mult_64      = constructMulByConstant(expr_n_64, 64, mprime_64);
+    typename SolverContext::result_type mulsh        = bvExtract(mult_64, 63, 32); //upper 32-bits    
+    typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh));
+    
+    // Improved variable arithmetic right shift: sign extend, shift, extract.
+    typename SolverContext::result_type extend_npm   = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh));    
+    typename SolverContext::result_type shift_npm    = bvVarRightShift(extend_npm, expr_shpost, 64);
+    typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits
+    
+    /////////////
+    
+    // XSIGN(n) is -1 if n is negative, positive one otherwise
+    typename SolverContext::result_type is_signed    = bvBoolExtract(expr_n, 31);
+    typename SolverContext::result_type neg_one      = bvMinusOne(32);
+    typename SolverContext::result_type xsign_of_n   = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32)));    
+
+    // q0 = (n_plus_mulsh >> shpost) - XSIGN(n)
+    typename SolverContext::result_type q0           = evaluate(_solver, bvsub(shift_shpost, xsign_of_n));    
+  
+    // n/d = (q0 ^ dsign) - dsign
+    typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign));    
+    typename SolverContext::result_type res          = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign));    
+    
+    return(res);
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
+    
+    typename SolverContext::result_type res;    
+    unsigned shift = amount & ((1 << shiftBits) - 1);
+
+    if (shift == 0) {
+        res = expr;
+    }
+    else if (shift >= width) {
+        res = bvZero(width);
+    }
+    else {
+        // stp shift does "expr @ [0 x s]" which we then have to extract,
+        // rolling our own gives slightly smaller exprs
+        res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr),
+                                       bvZero(shift)));
+    }
+
+    return(res);
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) {
+  
+    typename SolverContext::result_type res;    
+    unsigned shift = amount & ((1 << shiftBits) - 1);
+
+    if (shift == 0) {
+        res = expr;
+    } 
+    else if (shift >= width) {
+        res = bvZero(width);
+    }
+    else {
+        res = evaluate(_solver, concat(bvZero(shift),
+                                       extract(width - 1, shift, expr)));        
+    }
+
+    return(res);
+}
+
+// left shift by a variable amount on an expression of the specified width
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
+    
+    typename SolverContext::result_type res =  bvZero(width);
+    
+    int shiftBits = getShiftBits(width);
+
+    //get the shift amount (looking only at the bits appropriate for the given width)
+    typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount));    
+
+    //construct a big if-then-elif-elif-... with one case per possible shift amount
+    for(int i = width - 1; i >= 0; i--) {
+        res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
+                                                    bvLeftShift(expr, width, i, shiftBits),
+                                                    res));
+    }
+
+    return(res);
+}
+
+// logical right shift by a variable amount on an expression of the specified width
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
+    
+    typename SolverContext::result_type res = bvZero(width);
+    
+    int shiftBits = getShiftBits(width);
+    
+    //get the shift amount (looking only at the bits appropriate for the given width)
+    typename SolverContext::result_type shift = bvExtract(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 = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)),
+                                                    bvRightShift(expr, width, i, shiftBits),
+                                                    res));
+         // ToDo Reconsider widht to provide to bvRightShift
+    }
+
+    return(res);
+}
+
+// arithmetic right shift by a variable amount on an expression of the specified width
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) {
+  
+    int shiftBits = getShiftBits(width);
+
+    //get the shift amount (looking only at the bits appropriate for the given width)
+    typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0);
+    
+    //get the sign bit to fill with
+    typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1);
+
+    //start with the result if shifting by width-1
+    typename SolverContext::result_type res =  constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits);
+
+    // 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 = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)),
+                                                    constructAShrByConstant(expr, width, i, signedBool, shiftBits),
+                                                    res));
+    }
+
+    return(res);
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) {
+    typename SolverContext::result_type res = construct(e, 0);
+    _constructed.clear();
+    return res;
+}
+
+
+/** if *width_out!=1 then result is a bitvector,
+    otherwise it is a bool */
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) {
+  
+    if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) {
+        return(constructActual(e, width_out));
+    } else {
+        MetaSMTExprHashMapIter it = _constructed.find(e);
+        if (it != _constructed.end()) {
+            if (width_out) {
+                *width_out = it->second.second;
+            }
+            return it->second.first;
+        } else {
+            int width = 0;
+            if (!width_out) {
+                 width_out = &width;
+            }
+            typename SolverContext::result_type res = constructActual(e, width_out);
+            _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
+            return res;
+        }
+    }
+}
+
+template<typename SolverContext>
+typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out)  {
+
+    typename SolverContext::result_type res;
+    
+    int width = 0;
+    if (!width_out) { 
+        // assert(false);
+        width_out = &width;
+    }
+    
+    ++stats::queryConstructs;
+    
+//     std::cerr << "Constructing expression ";
+//     ExprPPrinter::printSingleExpr(std::cerr, e);
+//     std::cerr << "\n";
+
+    switch (e->getKind()) {    
+
+        case Expr::Constant:
+        {
+            ConstantExpr *coe = cast<ConstantExpr>(e);
+            assert(coe);
+            unsigned coe_width = coe->getWidth();
+            *width_out = coe_width;
+
+            // Coerce to bool if necessary.
+            if (coe_width == 1) {
+                res = (coe->isTrue()) ? getTrue() : getFalse();      
+            }
+            else if (coe_width <= 32) {
+                 res = bvConst32(coe_width, coe->getZExtValue(32));
+            }
+            else if (coe_width <= 64) {
+                 res = bvConst64(coe_width, coe->getZExtValue());
+            }
+            else {
+                 ref<ConstantExpr> tmp = coe;
+                 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());
+                     res = evaluate(_solver,
+                                    concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()),
+                                           res));
+                 }
+            }
+            break;
+        }
+
+        case Expr::NotOptimized:
+        { 
+            NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
+            assert(noe);
+            res = construct(noe->src, width_out);
+            break;
+        }
+	
+        case Expr::Select: 
+        {
+            SelectExpr *se = cast<SelectExpr>(e);
+            assert(se);
+            res = evaluate(_solver, 
+                           metaSMT::logic::Ite(construct(se->cond, 0), 
+                                               construct(se->trueExpr, width_out),
+                                               construct(se->falseExpr, width_out)));
+            break;
+        }
+
+        case Expr::Read:
+        {
+            ReadExpr *re = cast<ReadExpr>(e);
+            assert(re);
+            // FixMe call method of Array
+            *width_out = 8;
+            res = evaluate(_solver, 
+                           metaSMT::logic::Array::select(
+                                  getArrayForUpdate(re->updates.root, re->updates.head),
+                                  construct(re->index, 0)));
+            break;
+        }
+
+        case Expr::Concat:
+        {
+            ConcatExpr *ce = cast<ConcatExpr>(e);
+            assert(ce);
+            *width_out = ce->getWidth();
+            unsigned numKids = ce->getNumKids();
+
+            if (numKids > 0) {
+                res = evaluate(_solver, construct(ce->getKid(numKids-1), 0));
+                for (int i = numKids - 2; i >= 0; i--) {
+                    res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res));
+                }
+            }
+            break;
+        }
+
+        case Expr::Extract:
+        {
+            ExtractExpr *ee = cast<ExtractExpr>(e);
+            assert(ee);
+            // ToDo spare evaluate?
+            typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out));
+
+            unsigned ee_width = ee->getWidth();
+            *width_out = ee_width;
+
+            if (ee_width == 1) {
+                res = bvBoolExtract(child, ee->offset);
+            }
+            else {
+                res = evaluate(_solver,
+                               extract(ee->offset + ee_width - 1, ee->offset, child));
+            }
+            break;
+        }
+
+        case Expr::ZExt:
+        {
+            CastExpr *ce = cast<CastExpr>(e);
+            assert(ce);
+
+            int child_width = 0;
+            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));
+
+            unsigned ce_width = ce->getWidth();
+            *width_out = ce_width;
+
+            if (child_width == 1) {
+                res = evaluate(_solver, 
+                               metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width)));			                       
+            }
+            else {
+                res = evaluate(_solver, zero_extend(ce_width - child_width, child));
+            }
+
+            // ToDo calculate how many zeros to add
+            // Note: STP and metaSMT differ in the prototype arguments;
+            // STP requires the width of the resulting bv;
+            // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended
+            // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src)));
+    
+            break;	  
+        }
+  
+        case Expr::SExt:
+        {
+            CastExpr *ce = cast<CastExpr>(e);
+            assert(ce);
+    
+            int child_width = 0;
+            typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width));
+            
+            unsigned ce_width = ce->getWidth();
+            *width_out = ce_width;
+    
+            if (child_width == 1) {
+                res = evaluate(_solver, 
+                               metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width)));
+            }
+            else {
+                // ToDo ce_width - child_width? It is only ce_width in STPBuilder
+                res = evaluate(_solver, sign_extend(ce_width - child_width, child));
+            }
+
+            break;
+        }
+  
+        case Expr::Add:
+        {
+            AddExpr *ae = cast<AddExpr>(e);
+            assert(ae);	    
+            res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out)));
+            assert(*width_out != 1 && "uncanonicalized add");
+            break;	  
+        }  
+  
+        case Expr::Sub:  
+        {
+            SubExpr *se = cast<SubExpr>(e);
+            assert(se);	    
+            res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); 
+            assert(*width_out != 1 && "uncanonicalized sub");
+            break;	  
+        }  
+   
+        case Expr::Mul:
+        { 
+            MulExpr *me = cast<MulExpr>(e);
+            assert(me);
+    
+            typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out));
+            assert(*width_out != 1 && "uncanonicalized mul");
+    
+            ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left);
+            if (CE && (CE->getWidth() <= 64)) {	        		
+                res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue());		
+            }
+            else {
+                res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr));	     
+            }
+            break;
+        }
+
+        case Expr::UDiv:
+        {
+            UDivExpr *de = cast<UDivExpr>(e);
+            assert(de);
+
+            typename SolverContext::result_type left_expr = construct(de->left, width_out);
+            assert(*width_out != 1 && "uncanonicalized udiv");
+            bool construct_both = true;
+
+            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+            if (CE && (CE->getWidth() <= 64)) {
+                uint64_t divisor = CE->getZExtValue();
+                if (bits64::isPowerOfTwo(divisor)) {
+                    res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out));
+                    construct_both = false;
+                }
+                else if (_optimizeDivides) {
+                    if (*width_out == 32) { //only works for 32-bit division
+                        res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
+                        construct_both = false;
+                    }
+                }
+            }
+
+            if (construct_both) {	    
+                res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); 
+            }
+            break;
+        }
+
+        case Expr::SDiv:
+        {
+            SDivExpr *de = cast<SDivExpr>(e);
+            assert(de);
+
+            typename SolverContext::result_type left_expr = construct(de->left, width_out);
+            assert(*width_out != 1 && "uncanonicalized sdiv");
+
+            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+            if (CE && _optimizeDivides && (*width_out == 32)) {
+                res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32));
+            }
+            else {
+                res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); 
+            }
+            break;
+        }
+
+        case Expr::URem:
+        {
+            URemExpr *de = cast<URemExpr>(e);
+            assert(de);
+
+            typename SolverContext::result_type left_expr = construct(de->left, width_out);
+            assert(*width_out != 1 && "uncanonicalized urem");
+    
+            bool construct_both = true;
+            ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right);
+            if (CE && (CE->getWidth() <= 64)) {
+      
+                uint64_t divisor = CE->getZExtValue();
+
+                if (bits64::isPowerOfTwo(divisor)) {
+  
+                    unsigned bits = bits64::indexOfSingleBit(divisor);		  
+                    // special case for modding by 1 or else we bvExtract -1:0
+                    if (bits == 0) {
+                        res = bvZero(*width_out);
+                        construct_both = false;
+                    }
+                    else {
+                        res = evaluate(_solver, concat(bvZero(*width_out - bits), 
+                                                       bvExtract(left_expr, bits - 1, 0)));
+                        construct_both = false;
+                    }
+                }
+
+                // Use fast division to compute modulo without explicit division for constant divisor.
+       
+                if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division
+                    typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor);
+                    typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
+                    res = evaluate(_solver, bvsub(left_expr, quot_times_divisor));                    
+                    construct_both = false;
+                }
+            }
+    
+            if (construct_both) {
+                res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out)));	      
+            }
+            break;  
+        }
+
+        case Expr::SRem:
+        {
+            SRemExpr *de = cast<SRemExpr>(e);
+            assert(de);
+    
+            typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out));
+            typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out));
+            assert(*width_out != 1 && "uncanonicalized srem");
+    
+            bool construct_both = true;
+    
+#if 0 //not faster per first benchmark
+            
+            if (_optimizeDivides) {
+                if (ConstantExpr *cre = de->right->asConstant()) {
+                    uint64_t divisor = cre->asUInt64;
+    
+                    //use fast division to compute modulo without explicit division for constant divisor
+                    if( *width_out == 32 ) { //only works for 32-bit division
+                       	typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor);
+                        typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor);
+                        res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor );
+                        construct_both = false;
+                    }
+                }
+            }
+    
+#endif
+
+            if (construct_both) {     
+                res = evaluate(_solver, bvsrem(left_expr, right_expr));
+            }
+            break;
+        }
+
+        case Expr::Not:
+        {
+            NotExpr *ne = cast<NotExpr>(e);
+            assert(ne);
+    
+            typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out));
+            if (*width_out == 1) {
+                res = evaluate(_solver, metaSMT::logic::Not(child));
+            }
+            else {                
+                res = evaluate(_solver, bvnot(child));
+            }    
+            break;	  
+        }
+  
+        case Expr::And:
+        {
+            AndExpr *ae = cast<AndExpr>(e);
+	    assert(ae);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out));
+	    
+	    if (*width_out == 1) {
+	        res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr));
+	    }
+	    else {
+	        res = evaluate(_solver, bvand(left_expr, right_expr));
+	    }
+	    
+	    break;	  
+	}
+	  
+	case Expr::Or:
+	{
+	    OrExpr *oe = cast<OrExpr>(e);
+	    assert(oe);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out));
+	    
+	    if (*width_out == 1) {
+	        res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr));
+	    }
+	    else {
+	        res = evaluate(_solver, bvor(left_expr, right_expr));
+	    }
+	    
+	    break;	  
+	}
+	  
+	case Expr::Xor:
+	{
+	    XorExpr *xe = cast<XorExpr>(e);
+	    assert(xe);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out));
+	    
+	    if (*width_out == 1) {
+	        res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr));
+	    }
+	    else {
+	        res = evaluate(_solver, bvxor(left_expr, right_expr));
+	    }
+	    
+	    break;	  
+	}
+	  
+	case Expr::Shl:  
+	{	    
+	    ShlExpr *se = cast<ShlExpr>(e);
+	    assert(se);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
+	    assert(*width_out != 1 && "uncanonicalized shl");
+	    
+	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
+	        res =  bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
+            }
+            else {
+                int shiftWidth = 0;
+		typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth));
+		res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : 
+		                  evaluate(_solver, bvshl(left_expr, right_expr));	      
+	    }    
+	    
+	    break;	  
+	}
+	
+	case Expr::LShr:
+	{
+	    LShrExpr *lse = cast<LShrExpr>(e);
+	    assert(lse);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out));	    
+	    assert(*width_out != 1 && "uncanonicalized lshr");
+	    
+	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
+	        res =  bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out));
+	    }
+	    else {
+                int shiftWidth = 0;
+		typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth));
+		res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) :
+				  evaluate(_solver, bvshr(left_expr, right_expr));
+	    }
+	    
+	    break;	  
+	}
+	  
+	case Expr::AShr:  
+	{
+	    AShrExpr *ase = cast<AShrExpr>(e);
+	    assert(ase);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out));	    
+	    assert(*width_out != 1 && "uncanonicalized ashr");
+	    
+	    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+	        unsigned shift = (unsigned) CE->getLimitedValue();
+                typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1);
+		res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out));	      
+	    }
+	    else {
+                int shiftWidth = 0;
+		typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth));
+		res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) :
+		                  evaluate(_solver, bvashr(left_expr, right_expr)); 
+	    }    
+	    
+	    break;	  
+	}
+	  
+	case Expr::Eq: 
+	{
+	     EqExpr *ee = cast<EqExpr>(e);
+	     assert(ee);
+	     
+    	     typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out));
+	     typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out));
+
+	     if (*width_out==1) {
+	         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+		     if (CE->isTrue()) {
+		         res = right_expr;  
+		     }
+		     else {
+		         res = evaluate(_solver, metaSMT::logic::Not(right_expr));
+		     }
+		 }
+		 else {
+		     res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
+		 }
+	     } // end of *width_out == 1
+	     else {
+	         *width_out = 1;
+	         res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr));
+	     }
+	     
+	     break;
+	}
+	
+	case Expr::Ult:
+	{
+	    UltExpr *ue = cast<UltExpr>(e);
+	    assert(ue);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	    
+	    
+	    assert(*width_out != 1 && "uncanonicalized ult");
+	    *width_out = 1;    
+	    
+	    res = evaluate(_solver, bvult(left_expr, right_expr));
+	    break;	  
+	}
+	  
+	case Expr::Ule:
+	{
+	    UleExpr *ue = cast<UleExpr>(e);
+	    assert(ue);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out));	
+	    
+	    assert(*width_out != 1 && "uncanonicalized ule");
+	    *width_out = 1;    
+	    
+	    res = evaluate(_solver, bvule(left_expr, right_expr));
+	    break;	  
+	}
+	  
+	case Expr::Slt:
+	{
+	    SltExpr *se = cast<SltExpr>(e);
+	    assert(se);
+	    
+	    typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
+	    typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
+	    
+	    assert(*width_out != 1 && "uncanonicalized slt");
+	    *width_out = 1;
+	    
+	    res = evaluate(_solver, bvslt(left_expr, right_expr));
+	    break;	  
+	}
+	  
+        case Expr::Sle:
+        {
+            SleExpr *se = cast<SleExpr>(e);
+            assert(se);
+    
+            typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out));
+            typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out));	
+    
+            assert(*width_out != 1 && "uncanonicalized sle");
+            *width_out = 1;    
+    
+            res = evaluate(_solver, bvsle(left_expr, right_expr));
+            break;	  
+        }
+  
+        // unused due to canonicalization
+#if 0
+        case Expr::Ne:
+        case Expr::Ugt:
+        case Expr::Uge:
+        case Expr::Sgt:
+        case Expr::Sge:
+#endif  
+     
+        default:
+             assert(false);
+             break;      
+      
+    };
+    return res;
+}
+
+
+}  /* end of namespace klee */
+
+#endif /* SUPPORT_METASMT */
+
+#endif /* METASMTBUILDER_H_ */
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index e7187fc3..f2e38182 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -74,6 +74,7 @@ void QueryLoggingSolver::flushBuffer() {
               // we do additional check here to log only timeouts in case
               // user specified negative value for minQueryTimeToLog param
               os << logBuffer.str();              
+              os.flush();
           }                    
       }
       
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3414cda2..22b1545f 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -12,6 +12,7 @@
 
 #include "SolverStats.h"
 #include "STPBuilder.h"
+#include "MetaSMTBuilder.h"
 
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
@@ -20,6 +21,7 @@
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprUtil.h"
 #include "klee/Internal/Support/Timer.h"
+#include "klee/CommandLine.h"
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
@@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures",
 
 using namespace klee;
 
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+#endif /* SUPPORT_METASMT */
+
+
+
 /***/
 
 SolverImpl::~SolverImpl() {
@@ -809,3 +829,426 @@ STPSolverImpl::computeInitialValues(const Query &query,
 SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
    return runStatusCode;
 }
+
+#ifdef SUPPORT_METASMT
+
+// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
+
+template<typename SolverContext>
+class MetaSMTSolverImpl : public SolverImpl {
+private:
+
+  SolverContext _meta_solver;
+  MetaSMTSolver<SolverContext>  *_solver;  
+  MetaSMTBuilder<SolverContext> *_builder;
+  double _timeout;
+  bool   _useForked;
+  SolverRunStatus _runStatusCode;
+
+public:
+  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides);  
+  virtual ~MetaSMTSolverImpl();
+  
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout) { _timeout = timeout; }
+
+  bool computeTruth(const Query&, bool &isValid);
+  bool computeValue(const Query&, ref<Expr> &result);
+    
+  bool computeInitialValues(const Query &query,
+                            const std::vector<const Array*> &objects,
+                            std::vector< std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+    
+  SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr,
+                                           const std::vector<const Array*> &objects,
+                                           std::vector< std::vector<unsigned char> > &values,
+                                           bool &hasSolution);
+  
+  SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query,
+                                                 const std::vector<const Array*> &objects,
+                                                 std::vector< std::vector<unsigned char> > &values,
+                                                 bool &hasSolution,
+                                                 double timeout);
+  
+  SolverRunStatus getOperationStatusCode();
+  
+  SolverContext& get_meta_solver() { return(_meta_solver); };
+  
+};
+
+
+// ------------------------------------- MetaSMTSolver methods --------------------------------------------
+
+
+template<typename SolverContext>
+MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) 
+  : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides))
+{
+   
+}
+
+template<typename SolverContext>
+MetaSMTSolver<SolverContext>::~MetaSMTSolver()
+{
+  
+}
+
+template<typename SolverContext>
+char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) {
+  return(impl->getConstraintLog(query));
+}
+
+template<typename SolverContext>
+void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
+  impl->setCoreSolverTimeout(timeout);
+}
+
+
+// ------------------------------------- MetaSMTSolverImpl methods ----------------------------------------
+
+
+
+template<typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
+  : _solver(solver),    
+    _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)),
+    _timeout(0.0),
+    _useForked(useForked)
+{  
+  assert(_solver && "unable to create MetaSMTSolver");
+  assert(_builder && "unable to create MetaSMTBuilder");
+  
+  if (_useForked) {
+      shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
+      assert(shared_memory_id >= 0 && "shmget failed");
+      shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
+      assert(shared_memory_ptr != (void*) -1 && "shmat failed");
+      shmctl(shared_memory_id, IPC_RMID, NULL);
+  }
+}
+
+template<typename SolverContext>
+MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
+
+}
+
+template<typename SolverContext>
+char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
+  const char* msg = "Not supported";
+  char *buf = new char[strlen(msg) + 1];
+  strcpy(buf, msg);
+  return(buf);
+}
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) {  
+
+  bool success = false;
+  std::vector<const Array*> objects;
+  std::vector< std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  if (computeInitialValues(query, objects, values, hasSolution)) {
+      // query.expr is valid iff !query.expr is not satisfiable
+      isValid = !hasSolution;
+      success = true;
+  }
+
+  return(success);
+}
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) {
+  
+  bool success = false;
+  std::vector<const Array*> objects;
+  std::vector< std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  // Find the object used in the expression, and compute an assignment for them.
+  findSymbolicObjects(query.expr, objects);  
+  if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) {  
+      assert(hasSolution && "state has invalid constraint set");
+      // Evaluate the expression with the computed assignment.
+      Assignment a(objects, values);
+      result = a.evaluate(query.expr);
+      success = true;
+  }
+
+  return(success);
+}
+
+
+template<typename SolverContext>
+bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution) {  
+
+  _runStatusCode =  SOLVER_RUN_STATUS_FAILURE;
+
+  TimerStatIncrementer t(stats::queryTime);
+  assert(_builder);
+
+  /*
+   * FIXME push() and pop() work for Z3 but not for Boolector.
+   * If using Z3, use push() and pop() and assert constraints.
+   * If using Boolector, assume constrainsts instead of asserting them.
+   */
+  //push(_meta_solver);
+
+  if (!_useForked) {
+      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
+          //assertion(_meta_solver, _builder->construct(*it));
+          assumption(_meta_solver, _builder->construct(*it));  
+      }  
+  }  
+    
+  ++stats::queries;
+  ++stats::queryCounterexamples;  
+ 
+  bool success = true;
+  if (_useForked) {
+      _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout);
+      success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
+  }
+  else {
+      _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
+      success = true;
+  } 
+    
+  if (success) {
+      if (hasSolution) {
+          ++stats::queriesInvalid;
+      }
+      else {
+          ++stats::queriesValid;
+      }
+  }  
+   
+  //pop(_meta_solver); 
+  
+  return(success);
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr,
+                                             const std::vector<const Array*> &objects,
+                                             std::vector< std::vector<unsigned char> > &values,
+                                             bool &hasSolution)
+{
+
+  // assume the negation of the query  
+  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));  
+  hasSolution = solve(_meta_solver);  
+  
+  if (hasSolution) {
+      values.reserve(objects.size());
+      for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+        
+          const Array *array = *it;
+          assert(array);
+          typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
+           
+          std::vector<unsigned char> data;      
+          data.reserve(array->size);       
+           
+          for (unsigned offset = 0; offset < array->size; offset++) {
+              typename SolverContext::result_type elem_exp = evaluate(
+                       _meta_solver,
+                       metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+              unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
+              data.push_back(elem_value);
+          }
+                   
+          values.push_back(data);
+      }
+  }
+  
+  if (true == hasSolution) {
+      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
+  }
+  else {
+      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);  
+  }
+}
+
+static void metaSMTTimeoutHandler(int x) {
+  _exit(52);
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query,
+                                                          const std::vector<const Array*> &objects,
+                                                          std::vector< std::vector<unsigned char> > &values,
+                                                          bool &hasSolution,
+                                                          double timeout)
+{
+  unsigned char *pos = shared_memory_ptr;
+  unsigned sum = 0;
+  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+      sum += (*it)->size;    
+  }
+  // sum += sizeof(uint64_t);
+  sum += sizeof(stats::queryConstructs);
+  assert(sum < shared_memory_size && "not enough shared memory for counterexample");
+
+  fflush(stdout);
+  fflush(stderr);
+  int pid = fork();
+  if (pid == -1) {
+      fprintf(stderr, "error: fork failed (for metaSMT)");
+      return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED);
+  }
+  
+  if (pid == 0) {
+      if (timeout) {
+          ::alarm(0); /* Turn off alarm so we can safely set signal handler */
+          ::signal(SIGALRM, metaSMTTimeoutHandler);
+          ::alarm(std::max(1, (int) timeout));
+      }     
+      
+      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {      
+          assertion(_meta_solver, _builder->construct(*it));
+          //assumption(_meta_solver, _builder->construct(*it));  
+      } 
+      
+      
+      std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs;
+      if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
+          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+            
+              std::vector<typename SolverContext::result_type> aux_arr;          
+              const Array *array = *it;
+              assert(array);
+              typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
+              
+              for (unsigned offset = 0; offset < array->size; offset++) {
+                  typename SolverContext::result_type elem_exp = evaluate(
+                      _meta_solver,
+                      metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+                  aux_arr.push_back(elem_exp);
+              }
+              aux_arr_exprs.push_back(aux_arr);
+          }
+          assert(aux_arr_exprs.size() == objects.size());
+      }
+      
+           
+      // assume the negation of the query
+      // can be also asserted instead of assumed as we are in a child process
+      assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));        
+      unsigned res = solve(_meta_solver);
+
+      if (res) {
+
+          if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
+
+              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+
+                  const Array *array = *it;
+                  assert(array);
+                  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);      
+
+                  for (unsigned offset = 0; offset < array->size; offset++) {
+
+                      typename SolverContext::result_type elem_exp = evaluate(
+                          _meta_solver,
+                          metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
+                      unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
+                      *pos++ = elem_value;
+                  }
+              }
+          }
+          else {
+              typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end();
+              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) {
+                  const Array *array = *it;
+                  const std::vector<typename SolverContext::result_type>& arr_exp = *eit;
+                  assert(array);
+                  assert(array->size == arr_exp.size());
+
+                  for (unsigned offset = 0; offset < array->size; offset++) {
+                      unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]);
+                       *pos++ = elem_value;
+                  }
+              }
+          }
+      }
+      assert((uint64_t*) pos);
+      *((uint64_t*) pos) = stats::queryConstructs;      
+      
+      _exit(!res);
+  }
+  else {
+      int status;
+      pid_t res;
+
+      do {
+          res = waitpid(pid, &status, 0);
+      } 
+      while (res < 0 && errno == EINTR);
+    
+      if (res < 0) {
+          fprintf(stderr, "error: waitpid() for metaSMT failed");
+          return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED);
+      }
+      
+      // From timed_run.py: It appears that linux at least will on
+      // "occasion" return a status when the process was terminated by a
+      // signal, so test signal first.
+      if (WIFSIGNALED(status) || !WIFEXITED(status)) {
+           fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status));
+           return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED);
+      }
+
+      int exitcode = WEXITSTATUS(status);
+      if (exitcode == 0) {
+          hasSolution = true;
+      } 
+      else if (exitcode == 1) {
+          hasSolution = false;
+      }
+      else if (exitcode == 52) {
+          fprintf(stderr, "error: metaSMT timed out");
+          return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
+      }
+      else {
+          fprintf(stderr, "error: metaSMT did not return a recognized code");
+          return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE);
+      }
+      
+      if (hasSolution) {
+          values = std::vector< std::vector<unsigned char> >(objects.size());
+          unsigned i = 0;
+          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+              const Array *array = *it;
+              assert(array);
+              std::vector<unsigned char> &data = values[i++];
+              data.insert(data.begin(), pos, pos + array->size);
+              pos += array->size;
+          }
+      }
+      stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs);      
+
+      if (true == hasSolution) {
+          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+      }
+      else {
+          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+      }
+  }
+}
+
+template<typename SolverContext>
+SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
+   return _runStatusCode;
+}
+
+template class MetaSMTSolver< DirectSolver_Context < Boolector> >;
+template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
+template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
+
+#endif /* SUPPORT_METASMT */
+