3 files changed, 12 insertions, 10 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index 44f1afd4..dc0f135a 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -47,7 +47,7 @@ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER };
 extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 enum MetaSMTBackendType
 {
@@ -58,7 +58,7 @@ enum MetaSMTBackendType
 
 extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
 template <typename T>
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 978c901f..9d34e7b6 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -6,15 +6,18 @@
 /* Enable KLEE DEBUG checks */
 #undef ENABLE_KLEE_DEBUG
 
+/* Enable metaSMT API */
+#undef ENABLE_METASMT
+
+/* Using STP Solver backend */
+#undef ENABLE_STP
+
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
 /* Define to 1 if you have the <inttypes.h> header file. */
 #undef HAVE_INTTYPES_H
 
-/* Define to 1 if you have the `stp' library (-lstp). */
-#undef HAVE_LIBSTP
-
 /* Define if mallinfo() is available on this platform. */
 #undef HAVE_MALLINFO
 
@@ -93,7 +96,4 @@
 /* klee-uclibc is supported */
 #undef SUPPORT_KLEE_UCLIBC
 
-/* Supporting metaSMT API */
-#undef SUPPORT_METASMT
-
 #endif
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index e3adac6a..fed6191a 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -203,6 +203,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
   };
 
+#ifdef ENABLE_STP
   /// STPSolver - A complete solver based on STP.
   class STPSolver : public Solver {
   public:
@@ -222,9 +223,10 @@ namespace klee {
     /// is off.
     virtual void setCoreSolverTimeout(double timeout);
   };
+#endif // ENABLE_STP
 
   
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
   
   template<typename SolverContext>
   class MetaSMTSolver : public Solver {
@@ -236,7 +238,7 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
 };
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
   /* *** */