6 files changed, 40 insertions, 17 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index d7157b25..2f97b200 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,7 +73,7 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     llvm::cl::CommaSeparated
 );
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
     "metasmt-backend",
@@ -86,16 +86,31 @@ llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
         clEnumValEnd),
     llvm::cl::init(METASMT_BACKEND_STP));
 
-#endif /* SUPPORT_METASMT */
-
+#endif /* ENABLE_METASMT */
+
+// Pick the default core solver based on configuration
+#ifdef ENABLE_STP
+#define STP_IS_DEFAULT_STR " (default)"
+#define METASMT_IS_DEFAULT_STR ""
+#define DEFAULT_CORE_SOLVER STP_SOLVER
+#elif ENABLE_METASMT
+#define STP_IS_DEFAULT_STR ""
+#define METASMT_IS_DEFAULT_STR " (default)"
+#define DEFAULT_CORE_SOLVER METASMT_SOLVER
+#else
+#error "Unsupported solver configuration"
+#endif
 llvm::cl::opt<CoreSolverType> CoreSolverToUse(
     "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"),
-    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"),
-                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
+    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR),
+                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR),
                      clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
                      clEnumValEnd),
-    llvm::cl::init(STP_SOLVER));
+    llvm::cl::init(DEFAULT_CORE_SOLVER));
 }
+#undef STP_IS_DEFAULT_STR
+#undef METASMT_IS_DEFAULT_STR
+#undef DEFAULT_CORE_SOLVER
 
 
 
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
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index 6da1b492..ffd3cfe9 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -15,7 +15,7 @@
 #include "klee/util/ExprHashMap.h"
 #include "ConstantDivision.h"
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include "llvm/Support/CommandLine.h"
 
@@ -1177,6 +1177,6 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
 
 }  /* end of namespace klee */
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 #endif /* METASMTBUILDER_H_ */
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 8394bbf3..971ef371 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -6,8 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
-#ifdef SUPPORT_METASMT
+#include "klee/Config/config.h"
+#ifdef ENABLE_METASMT
 
 #include "MetaSMTBuilder.h"
 #include "klee/Constraints.h"
@@ -463,4 +463,4 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
-#endif // SUPPORT_METASMT
+#endif // ENABLE_METASMT
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 2f51c2b9..2b07f391 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 
 #include "klee/Expr.h"
@@ -902,5 +903,5 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return vc_trueExpr(vc);
   }
 }
-
+#endif // ENABLE_STP
 
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index cb15a23c..5c49521e 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -6,7 +6,8 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-
+#include "klee/Config/config.h"
+#ifdef ENABLE_STP
 #include "STPBuilder.h"
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
@@ -382,3 +383,4 @@ void STPSolver::setCoreSolverTimeout(double timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
+#endif // ENABLE_STP