diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-12 20:14:01 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 11:50:09 +0000 |
| commit | 8a7705ad979096d4e611fb2b8b397c48dd5fffc1 (patch) | |
| tree | 86a2fd486e2bca162d4b4f3aa0d3b90927f76e1d /lib/Solver/CoreSolver.cpp | |
| parent | e81f5ceed580d4d267e3c857b47637d6bd065499 (diff) | |
| download | klee-8a7705ad979096d4e611fb2b8b397c48dd5fffc1.tar.gz | |
Make it possible to build KLEE without using STP and only MetaSMT.
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
Diffstat (limited to 'lib/Solver/CoreSolver.cpp')
| -rw-r--r-- | lib/Solver/CoreSolver.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 9d21931d..0d451f27 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -13,7 +13,7 @@ #include "llvm/Support/raw_ostream.h" #include <string> -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT #include <metaSMT/frontend/Array.hpp> #include <metaSMT/backend/Z3_Backend.hpp> @@ -61,17 +61,22 @@ static Solver *handleMetaSMT() { llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; return coreSolver; } -#endif /* SUPPORT_METASMT */ +#endif /* ENABLE_METASMT */ namespace klee { Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: +#ifdef ENABLE_STP llvm::errs() << "Using STP solver backend\n"; return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#else + llvm::errs() << "Not compiled with STP support\n"; + return NULL; +#endif case METASMT_SOLVER: -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT llvm::errs() << "Using MetaSMT solver backend\n"; return handleMetaSMT(); #else |