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.

19 files changed, 169 insertions, 107 deletions

diff --git a/Makefile.common b/Makefile.common
index 7b210118..4ec1d4c6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -61,7 +61,11 @@ endif
 # This is filename that KLEE will look for when trying to load klee-uclibc
 KLEE_UCLIBC_BCA_NAME="klee-uclibc.bca"
 
-CXX.Flags += $(STP_CFLAGS)
+ifneq ($(ENABLE_STP),0)
+  CXX.Flags += $(STP_CFLAGS)
+  CXX.Flags += -DEXT_HASH_MAP
+endif
+
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_INSTALL_BIN_DIR=\"$(PROJ_bindir)\"
 CXX.Flags += -DKLEE_INSTALL_RUNTIME_DIR=\"$(BYTECODE_DESTINATION)\"
 
@@ -69,9 +73,6 @@ ifeq ($(ENABLE_UCLIBC),1)
 	CXX.Flags += -DKLEE_UCLIBC_BCA_NAME=\"$(KLEE_UCLIBC_BCA_NAME)\"
 endif
 
-# For STP.
-CXX.Flags += -DEXT_HASH_MAP
-
 # For metaSMT
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/Makefile.config.in b/Makefile.config.in
index 5b9f929c..745b4cc1 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -29,6 +29,7 @@ PROJ_INSTALL_ROOT := @prefix@
 
 KLEE_USE_CXX11 := @KLEE_USE_CXX11@
 
+ENABLE_STP := @ENABLE_STP@
 STP_CFLAGS := @STP_CFLAGS@
 STP_LDFLAGS := @STP_LDFLAGS@
 
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 3d4becc8..8ba6a029 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -553,58 +553,70 @@ dnl **************************************************************************
 dnl Find an install of STP
 dnl **************************************************************************
 
+ENABLE_STP=0
 AC_ARG_WITH(stp,
   AS_HELP_STRING([--with-stp],
     [Location of STP installation directory]),[
       #Check for empty argument
       if test "X$withval" = X ; then
-	      AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
+        AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
       fi
       stp_root=`(cd $withval && pwd) 2> /dev/null`
 
       #Check for bad path
       if test "X$stp_root" = X ; then
-	    AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
+        AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
       fi
 
       STP_CFLAGS="-I$stp_root/include"
       STP_LDFLAGS="-L$stp_root/lib"
+      ENABLE_STP=1
     ])
 
-old_CPPFLAGS="$CPPFLAGS"
-CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
-AC_CHECK_HEADER(stp/c_interface.h,,
-    [
-        AC_MSG_ERROR([Unable to use stp/c_interface.h header])
-    ])
-CPPFLAGS="$old_CPPFLAGS"
-
-STP_NEEDS_MINISAT=0
-AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
-       STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp])
-], "$STP_LDFLAGS")
-
-dnl Try linking again with minisat if necessary
-if test "X$STP_NEEDS_MINISAT" != X0 ; then
-  # Need to clear cached result
-  unset ac_cv_lib_stp_vc_setInterfaceFlags
-
-  AC_CHECK_LIB(stp,
-	       vc_setInterfaceFlags,, [
-	       AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
-  ], "$STP_LDFLAGS" "-lminisat" )
-
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+if test "X$ENABLE_STP" != X0; then
+    old_CPPFLAGS="$CPPFLAGS"
+    CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
+    AC_CHECK_HEADER(stp/c_interface.h,,
+        [
+            AC_MSG_ERROR([Unable to use stp/c_interface.h header])
+        ])
+
+    dnl we use [:] as a no-op so that AC_CHECK_LIB doesn't append -lstp
+    dnl automatically which would break subsequent uses of AC_CHECK_LIB()
+    STP_NEEDS_MINISAT=0
+    AC_CHECK_LIB(stp, vc_setInterfaceFlags, [:], [
+           STP_NEEDS_MINISAT=1; AC_MSG_RESULT([Could not link with libstp])
+    ], "$STP_LDFLAGS")
+    CPPFLAGS="$old_CPPFLAGS"
+
+    dnl Try linking again with minisat if necessary
+    if test "X$STP_NEEDS_MINISAT" != X0 ; then
+      # Need to clear cached result
+      unset ac_cv_lib_stp_vc_setInterfaceFlags
+
+      AC_CHECK_LIB(stp,
+               vc_setInterfaceFlags,[:], [
+               AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
+      ], "$STP_LDFLAGS" "-lminisat" )
+
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+    else
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    fi
+    AC_MSG_NOTICE([Using STP solver backend])
+    CPPFLAGS="$old_CPPFLAGS"
+    AC_DEFINE(ENABLE_STP, [1], [Using STP Solver backend])
 else
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    AC_MSG_NOTICE([Not using STP solver backend])
 fi
 
-
+AC_SUBST(ENABLE_STP)
 AC_SUBST(STP_CFLAGS)
 AC_SUBST(STP_LDFLAGS)
 
+
 dnl **************************************************************************
-dnl User option to enable metaSMT constraint solvers and to specify the 
+dnl User option to enable metaSMT constraint solvers and to specify the
 dnl the location of the metaSMT root directory
 dnl **************************************************************************
 
@@ -613,13 +625,13 @@ AC_ARG_WITH(metasmt,
     [Location of metaSMT installation directory]),,)
 
 if test X$with_metasmt = X ; then
-  AC_SUBST(ENABLE_METASMT,[[0]])
+  ENABLE_METASMT=0
 else
   metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
 
   dnl AC_LANG(C++)
   old_CPPFLAGS="$CPPFLAGS"
-  old_LDFLAGS="$LDFLAGS"  
+  old_LDFLAGS="$LDFLAGS"
   CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
   LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
   AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [
@@ -627,14 +639,24 @@ else
   ])
   AC_LINK_IFELSE(
       [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])],
-      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])  
+      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])
   CPPFLAGS="$old_CPPFLAGS"
   LDFLAGS="$old_LDFLAGS"
 
-  AC_DEFINE(SUPPORT_METASMT, 1, [Supporting metaSMT API])
-  AC_SUBST(ENABLE_METASMT,[[1]])
+  AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API])
   AC_SUBST(METASMT_ROOT,$metasmt_root)
   AC_SUBST(REQUIRES_RTTI,[[1]])
+  ENABLE_METASMT=1
+fi
+
+AC_SUBST(ENABLE_METASMT)
+
+dnl **************************************************************************
+dnl Check at least one solver backend is enabled
+dnl **************************************************************************
+
+if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then
+    AC_MSG_ERROR([At least one solver backend must be enabled, try using --with-stp or --with-metasmt])
 fi
 
 
diff --git a/configure b/configure
index 72ed1883..af871ce6 100755
--- a/configure
+++ b/configure
@@ -624,10 +624,11 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
-METASMT_ROOT
 ENABLE_METASMT
+METASMT_ROOT
 STP_LDFLAGS
 STP_CFLAGS
+ENABLE_STP
 CXXCPP
 HAVE_SELINUX
 EGREP
@@ -4865,43 +4866,45 @@ fi
 
 
 
+ENABLE_STP=0
 
 # Check whether --with-stp was given.
 if test "${with_stp+set}" = set; then :
   withval=$with_stp;
       #Check for empty argument
       if test "X$withval" = X ; then
-	      as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
+        as_fn_error $? "<path> cannot be empty in --with-stp=<path>" "$LINENO" 5
       fi
       stp_root=`(cd $withval && pwd) 2> /dev/null`
 
       #Check for bad path
       if test "X$stp_root" = X ; then
-	    as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
+        as_fn_error $? "Cannot access path $with_stp passed to --with-stp" "$LINENO" 5
       fi
 
       STP_CFLAGS="-I$stp_root/include"
       STP_LDFLAGS="-L$stp_root/lib"
+      ENABLE_STP=1
 
 fi
 
 
-old_CPPFLAGS="$CPPFLAGS"
-CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
-ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
+if test "X$ENABLE_STP" != X0; then
+    old_CPPFLAGS="$CPPFLAGS"
+    CPPFLAGS="$CPPFLAGS $STP_CFLAGS"
+    ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
 if test "x$ac_cv_header_stp_c_interface_h" = xyes; then :
 
 else
 
-        as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
+            as_fn_error $? "Unable to use stp/c_interface.h header" "$LINENO" 5
 
 fi
 
 
-CPPFLAGS="$old_CPPFLAGS"
 
-STP_NEEDS_MINISAT=0
-{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+            STP_NEEDS_MINISAT=0
+    { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
 if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
   $as_echo_n "(cached) " >&6
@@ -4938,25 +4941,21 @@ fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
 if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
-  cat >>confdefs.h <<_ACEOF
-#define HAVE_LIBSTP 1
-_ACEOF
-
-  LIBS="-lstp $LIBS"
-
+  :
 else
 
-       STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5
+           STP_NEEDS_MINISAT=1; { $as_echo "$as_me:${as_lineno-$LINENO}: result: Could not link with libstp" >&5
 $as_echo "Could not link with libstp" >&6; }
 
 fi
 
+    CPPFLAGS="$old_CPPFLAGS"
 
-if test "X$STP_NEEDS_MINISAT" != X0 ; then
-  # Need to clear cached result
-  unset ac_cv_lib_stp_vc_setInterfaceFlags
+        if test "X$STP_NEEDS_MINISAT" != X0 ; then
+      # Need to clear cached result
+      unset ac_cv_lib_stp_vc_setInterfaceFlags
 
-  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
+      { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
 if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
   $as_echo_n "(cached) " >&6
@@ -4993,22 +4992,27 @@ fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
 if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
-  cat >>confdefs.h <<_ACEOF
-#define HAVE_LIBSTP 1
-_ACEOF
-
-  LIBS="-lstp $LIBS"
-
+  :
 else
 
-	       as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5
+               as_fn_error $? "Unable to link with libstp. Check config.log to see what went wrong" "$LINENO" 5
 
 fi
 
 
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp -lminisat"
+    else
+      STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    fi
+    { $as_echo "$as_me:${as_lineno-$LINENO}: Using STP solver backend" >&5
+$as_echo "$as_me: Using STP solver backend" >&6;}
+    CPPFLAGS="$old_CPPFLAGS"
+
+$as_echo "#define ENABLE_STP 1" >>confdefs.h
+
 else
-  STP_LDFLAGS="${STP_LDFLAGS} -lstp"
+    { $as_echo "$as_me:${as_lineno-$LINENO}: Not using STP solver backend" >&5
+$as_echo "$as_me: Not using STP solver backend" >&6;}
 fi
 
 
@@ -5017,6 +5021,7 @@ fi
 
 
 
+
 # Check whether --with-metasmt was given.
 if test "${with_metasmt+set}" = set; then :
   withval=$with_metasmt;
@@ -5025,7 +5030,6 @@ fi
 
 if test X$with_metasmt = X ; then
   ENABLE_METASMT=0
-
 else
   metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
 
@@ -5073,14 +5077,20 @@ rm -f core conftest.err conftest.$ac_objext \
   LDFLAGS="$old_LDFLAGS"
 
 
-$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h
-
-  ENABLE_METASMT=1
+$as_echo "#define ENABLE_METASMT 1" >>confdefs.h
 
   METASMT_ROOT=$metasmt_root
 
   REQUIRES_RTTI=1
 
+  ENABLE_METASMT=1
+fi
+
+
+
+
+if test "X$ENABLE_STP$ENABLE_METASMT" == X00 ; then
+    as_fn_error $? "At least one solver backend must be enabled, try using --with-stp or --with-metasmt" "$LINENO" 5
 fi
 
 
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 */
 
   /* *** */
 
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
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 10b19a20..a72c4c9d 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -19,7 +19,9 @@ LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index f91693c5..ea9be41f 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -36,7 +36,7 @@ using namespace llvm;
 using namespace klee;
 using namespace klee::expr;
 
-#ifdef SUPPORT_METASMT
+#ifdef ENABLE_METASMT
 
 #include <metaSMT/DirectSolver_Context.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
@@ -53,7 +53,7 @@ using namespace klee::expr;
 using namespace metaSMT;
 using namespace metaSMT::solver;
 
-#endif /* SUPPORT_METASMT */
+#endif /* ENABLE_METASMT */
 
 
 
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index eb80d845..8e9ac6b7 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -20,7 +20,9 @@ LINK_COMPONENTS += irreader
 endif
 include $(LEVEL)/Makefile.common
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif
 
 ifeq ($(ENABLE_METASMT),1)
   include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
index e52aea31..ca92271a 100644
--- a/unittests/Expr/Makefile
+++ b/unittests/Expr/Makefile
@@ -10,4 +10,3 @@ LINK_COMPONENTS := support
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
 CXXFLAGS += -DLLVM_29_UNITTEST
-LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Ref/Makefile b/unittests/Ref/Makefile
index 14dcc8bd..10c4bebd 100644
--- a/unittests/Ref/Makefile
+++ b/unittests/Ref/Makefile
@@ -8,5 +8,3 @@ USEDLIBS := kleaverExpr.a kleeBasic.a
 LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
-
-LIBS += $(STP_LDFLAGS)
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
index aeac34ac..65edbe7a 100644
--- a/unittests/Solver/Makefile
+++ b/unittests/Solver/Makefile
@@ -9,4 +9,6 @@ LINK_COMPONENTS := support
 
 include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
 
-LIBS += $(STP_LDFLAGS)
+ifneq ($(ENABLE_STP),0)
+  LIBS += $(STP_LDFLAGS)
+endif