9 files changed, 47 insertions, 17 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 38b22c6f..c4c70069 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -7,6 +7,7 @@
 #define KLEE_COMMANDLINE_H
 
 #include "llvm/Support/CommandLine.h"
+#include "klee/Config/config.h"
 
 namespace klee {
 
@@ -43,6 +44,19 @@ enum QueryLoggingSolverType
  */
 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
+#ifdef SUPPORT_METASMT
+
+enum MetaSMTBackendType
+{
+    METASMT_BACKEND_NONE,
+    METASMT_BACKEND_STP,
+    METASMT_BACKEND_Z3,
+    METASMT_BACKEND_BOOLECTOR
+};
+
+extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT;
+
+#endif /* SUPPORT_METASMT */
 
 //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
 template <typename T>
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 0f79e01d..0a94de8f 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -81,4 +81,7 @@
 /* Define to 1 if you have the ANSI C header files. */
 #undef STDC_HEADERS
 
+/* Supporting metaSMT API */
+#undef SUPPORT_METASMT
+
 #endif
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index 20db560d..fc86070b 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -11,11 +11,7 @@
 #define KLEE_KINSTRUCTION_H
 
 #include "klee/Config/Version.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
-#include "llvm/System/DataTypes.h"
-#else
 #include "llvm/Support/DataTypes.h"
-#endif
 #include <vector>
 
 namespace llvm {
diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h
index 1d305374..f1f16c5e 100644
--- a/include/klee/Internal/Support/FloatEvaluation.h
+++ b/include/klee/Internal/Support/FloatEvaluation.h
@@ -17,6 +17,8 @@
 
 #include "llvm/Support/MathExtras.h"
 
+#include <cassert>
+
 namespace klee {
 namespace floats {
 
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index e29db411..e93284d6 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -51,11 +51,13 @@ public:
     std::string LibraryDir;
     bool Optimize;
     bool CheckDivZero;
+    bool CheckOvershift;
 
     ModuleOptions(const std::string& _LibraryDir, 
-                  bool _Optimize, bool _CheckDivZero)
+                  bool _Optimize, bool _CheckDivZero,
+                  bool _CheckOvershift)
       : LibraryDir(_LibraryDir), Optimize(_Optimize), 
-        CheckDivZero(_CheckDivZero) {}
+        CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
   };
 
   enum LogType
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 8fe33c7c..00e4c962 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -219,6 +219,21 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
   };
 
+  
+#ifdef SUPPORT_METASMT
+  
+  template<typename SolverContext>
+  class MetaSMTSolver : public Solver {
+  public:
+    MetaSMTSolver(bool useForked, bool optimizeDivides);
+    virtual ~MetaSMTSolver();
+  
+    virtual char *getConstraintLog(const Query&);
+    virtual void setCoreSolverTimeout(double timeout);
+};
+
+#endif /* SUPPORT_METASMT */
+
   /* *** */
 
   /// createValidatingSolver - Create a solver which will validate all query
diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h
index 1e5b1c92..6b8fb165 100644
--- a/include/klee/Statistic.h
+++ b/include/klee/Statistic.h
@@ -11,11 +11,7 @@
 #define KLEE_STATISTIC_H
 
 #include "klee/Config/Version.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
-#include "llvm/System/DataTypes.h"
-#else
 #include "llvm/Support/DataTypes.h"
-#endif
 #include <string>
 
 namespace klee {
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
index aa78e534..f228b289 100644
--- a/include/klee/util/Bits.h
+++ b/include/klee/util/Bits.h
@@ -11,11 +11,7 @@
 #define KLEE_UTIL_BITS_H
 
 #include "klee/Config/Version.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
-#include "llvm/System/DataTypes.h"
-#else
 #include "llvm/Support/DataTypes.h"
-#endif
 
 namespace klee {
   namespace bits32 {
diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h
index 4446914d..2d145cd6 100644
--- a/include/klee/util/GetElementPtrTypeIterator.h
+++ b/include/klee/util/GetElementPtrTypeIterator.h
@@ -18,15 +18,21 @@
 #ifndef KLEE_UTIL_GETELEMENTPTRTYPE_H
 #define KLEE_UTIL_GETELEMENTPTRTYPE_H
 
-#include "klee/Config/Version.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/User.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Constants.h"
+#else
 #include "llvm/User.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Instructions.h"
-#include "klee/Config/Version.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
 #include "llvm/Constants.h"
 #endif
+#endif
+
+#include "klee/Config/Version.h"
 
 namespace klee {
   template<typename ItTy = llvm::User::const_op_iterator>