5 files changed, 19 insertions, 11 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
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