4 files changed, 97 insertions, 4 deletions
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index b6ccc91f..b93e361d 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -20,3 +20,14 @@ LINK_COMPONENTS = support
 include $(LEVEL)/Makefile.common
 
 LIBS += -lstp
+
+ifeq ($(ENABLE_METASMT),1)
+  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
+  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
+              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
+              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
+              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib 
+  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) 
+  LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core
+endif
\ No newline at end of file
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index accc48e4..f5bbfaf0 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -45,6 +45,28 @@ using namespace llvm;
 using namespace klee;
 using namespace klee::expr;
 
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.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 {
   llvm::cl::opt<std::string>
   InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional,
@@ -211,7 +233,39 @@ static bool EvaluateInputAST(const char *Filename,
     return false;
 
   // FIXME: Support choice of solver.
-  Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  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 = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  }
+#else
+  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+#endif /* SUPPORT_METASMT */
+  
   
   if (!UseDummySolver) {
     if (0 != MaxCoreSolverTime) {
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 01486fef..f050bf74 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -15,6 +15,20 @@ include $(LEVEL)/Makefile.config
 USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a  kleaverSolver.a kleaverExpr.a kleeSupport.a 
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
+ifeq ($(shell echo "$(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3" | bc), 1)
+LINK_COMPONENTS += irreader
+endif
 include $(LEVEL)/Makefile.common
 
 LIBS += -lstp
+
+ifeq ($(ENABLE_METASMT),1)
+  include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
+  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
+              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
+              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
+              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib 
+  CXX.Flags += -DBOOST_HAS_GCC_TR1
+  CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) 
+  LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core
+endif
\ No newline at end of file
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 7cd61788..0e576415 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -13,11 +13,17 @@
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
 
+#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Type.h"
+#include "llvm/IR/InstrTypes.h"
+#include "llvm/IR/Instruction.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/LLVMContext.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Module.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-#include "llvm/ModuleProvider.h"
-#endif
 #include "llvm/Type.h"
 #include "llvm/InstrTypes.h"
 #include "llvm/Instruction.h"
@@ -25,6 +31,10 @@
 #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
+#endif
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
+#include "llvm/ModuleProvider.h"
+#endif
 #include "llvm/Bitcode/ReaderWriter.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/ManagedStatic.h"
@@ -1256,7 +1266,11 @@ int main(int argc, char **argv, char **envp) {
   case KleeLibc: {
     // FIXME: Find a reasonable solution for this.
     llvm::sys::Path Path(Opts.LibraryDir);
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    Path.appendComponent("klee-libc.bc");
+#else
     Path.appendComponent("libklee-libc.bca");
+#endif
     mainModule = klee::linkWithLibrary(mainModule, Path.c_str());
     assert(mainModule && "unable to link with klee-libc");
     break;