about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-01-14 12:27:53 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2016-01-14 12:30:45 +0000
commitb9453efe7ca4c838e5f31e682792eda6259133a6 (patch)
tree15535bc70d0743892cefaf5b49a262c525bef68d
parentcece05cadf6a624afd188e81720ae7701736a703 (diff)
downloadklee-b9453efe7ca4c838e5f31e682792eda6259133a6.tar.gz
Remove unnecessary MetaSMT includes from kleaver's ``main.cpp``.
-rw-r--r--tools/kleaver/main.cpp22
1 files changed, 0 insertions, 22 deletions
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index ea9be41f..edc5f4c9 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -36,28 +36,6 @@ using namespace llvm;
 using namespace klee;
 using namespace klee::expr;
 
-#ifdef ENABLE_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 /* ENABLE_METASMT */
-
-
-
-
 namespace {
   llvm::cl::opt<std::string>
   InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional,