diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 12:27:53 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 12:30:45 +0000 |
commit | b9453efe7ca4c838e5f31e682792eda6259133a6 (patch) | |
tree | 15535bc70d0743892cefaf5b49a262c525bef68d | |
parent | cece05cadf6a624afd188e81720ae7701736a703 (diff) | |
download | klee-b9453efe7ca4c838e5f31e682792eda6259133a6.tar.gz |
Remove unnecessary MetaSMT includes from kleaver's ``main.cpp``.
-rw-r--r-- | tools/kleaver/main.cpp | 22 |
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, |