Add option to use an external version of STP

This patch adds a new configure option, --with-stp, which configures
KLEE to use an external version of STP instead of the version in the
source tree.  It includes documentation referring users to the STP
download location.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8

11 files changed, 410 insertions, 8 deletions

diff --git a/Makefile b/Makefile
index 2c3ab72b..44a9b836 100644
--- a/Makefile
+++ b/Makefile
@@ -12,7 +12,13 @@
 #
 LEVEL = .
 
-DIRS = stp lib tools runtime
+include $(LEVEL)/Makefile.config
+
+DIRS = lib
+ifeq ($(ENABLE_EXT_STP),0)
+  DIRS += stp
+endif
+DIRS += tools runtime
 EXTRA_DIST = include
 
 # Only build support directories when building unittests.
diff --git a/Makefile.common b/Makefile.common
index f3a8f8be..ff83602c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -26,8 +26,13 @@ LLVMCC := $(LLVMGCC)
 LLVMCXX := $(LLVMGXX)
 endif
 
-LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
-CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+ifeq ($(ENABLE_EXT_STP),1)
+  LD.Flags += -L$(STP_ROOT)/lib
+  CXX.Flags += -I$(STP_ROOT)/include
+else
+  LD.Flags += -L$(PROJ_SRC_ROOT)/stp/lib
+  CXX.Flags += -I$(PROJ_SRC_ROOT)/stp/include
+endif
 CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\"
 
 # For STP.
diff --git a/Makefile.config.in b/Makefile.config.in
index 0b858831..4d9718db 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -20,6 +20,9 @@ PROJ_OBJ_ROOT := $(subst //,/,@abs_top_objdir@)
 # Set the root directory of this project's install prefix
 PROJ_INSTALL_ROOT := @prefix@
 
+ENABLE_EXT_STP := @ENABLE_EXT_STP@
+STP_ROOT := @STP_ROOT@
+
 ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
 ENABLE_STPLOG := @ENABLE_STPLOG@
 ENABLE_UCLIBC := @ENABLE_UCLIBC@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 4266ac47..015c4f44 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -262,6 +262,31 @@ AC_CHECK_HEADERS([selinux/selinux.h],
         AC_SUBST(HAVE_SELINUX, 1),
         AC_SUBST(HAVE_SELINUX, 0))
 
+AC_ARG_WITH(stp,
+  AS_HELP_STRING([--with-stp],
+    [Location of STP installation directory]),,)
+
+if test X$with_stp = X ; then
+  AC_SUBST(ENABLE_EXT_STP,[[0]])
+else
+  stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+  old_CPPFLAGS="$CPPFLAGS"
+  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
+  AC_CHECK_HEADER(stp/c_interface.h,, [
+         AC_MSG_ERROR([Unable to use stp/c_interface.h header])
+  ])
+  CPPFLAGS="$old_CPPFLAGS"
+
+  AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
+         AC_MSG_ERROR([Unable to link with libstp])
+  ], -L$stp_root/lib)
+
+  AC_DEFINE(HAVE_EXT_STP, 1, [Using external STP])
+  AC_SUBST(ENABLE_EXT_STP,[[1]])
+  AC_SUBST(STP_ROOT,$stp_root)
+fi
+
 dnl **************************************************************************
 dnl * Create the output files
 dnl **************************************************************************
diff --git a/configure b/configure
index 4f24a6b6..e1622458 100755
--- a/configure
+++ b/configure
@@ -674,6 +674,8 @@ CXX
 CXXFLAGS
 ac_ct_CXX
 CXXCPP
+ENABLE_EXT_STP
+STP_ROOT
 LIBOBJS
 LTLIBOBJS'
 ac_subst_files=''
@@ -1275,6 +1277,7 @@ Optional Packages:
   --with-uclibc           Enable use of the klee uclibc at the given path
   --with-runtime          Select build configuration for runtime libraries
                           (default Release)
+  --with-stp              Location of STP installation directory
 
 Some influential environment variables:
   CC          C compiler command
@@ -4952,6 +4955,293 @@ done
 
 
 
+# Check whether --with-stp was given.
+if test "${with_stp+set}" = set; then
+  withval=$with_stp;
+fi
+
+
+if test X$with_stp = X ; then
+  ENABLE_EXT_STP=0
+
+else
+  stp_root=`cd $with_stp 2> /dev/null; pwd`
+
+  old_CPPFLAGS="$CPPFLAGS"
+  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
+  if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  { echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+else
+  # Is the header compilable?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h usability" >&5
+echo $ECHO_N "checking stp/c_interface.h usability... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h.  */
+$ac_includes_default
+#include <stp/c_interface.h>
+_ACEOF
+rm -f conftest.$ac_objext
+if { (ac_try="$ac_compile"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_compile") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } &&
+	 { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; } &&
+	 { ac_try='test -s conftest.$ac_objext'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; }; then
+  ac_header_compiler=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	ac_header_compiler=no
+fi
+
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_compiler" >&5
+echo "${ECHO_T}$ac_header_compiler" >&6; }
+
+# Is the header present?
+{ echo "$as_me:$LINENO: checking stp/c_interface.h presence" >&5
+echo $ECHO_N "checking stp/c_interface.h presence... $ECHO_C" >&6; }
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h.  */
+#include <stp/c_interface.h>
+_ACEOF
+if { (ac_try="$ac_cpp conftest.$ac_ext"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_cpp conftest.$ac_ext") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } >/dev/null; then
+  if test -s conftest.err; then
+    ac_cpp_err=$ac_cxx_preproc_warn_flag
+    ac_cpp_err=$ac_cpp_err$ac_cxx_werror_flag
+  else
+    ac_cpp_err=
+  fi
+else
+  ac_cpp_err=yes
+fi
+if test -z "$ac_cpp_err"; then
+  ac_header_preproc=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+  ac_header_preproc=no
+fi
+
+rm -f conftest.err conftest.$ac_ext
+{ echo "$as_me:$LINENO: result: $ac_header_preproc" >&5
+echo "${ECHO_T}$ac_header_preproc" >&6; }
+
+# So?  What about this header?
+case $ac_header_compiler:$ac_header_preproc:$ac_cxx_preproc_warn_flag in
+  yes:no: )
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&5
+echo "$as_me: WARNING: stp/c_interface.h: accepted by the compiler, rejected by the preprocessor!" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the compiler's result" >&2;}
+    ac_header_preproc=yes
+    ;;
+  no:yes:* )
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: present but cannot be compiled" >&5
+echo "$as_me: WARNING: stp/c_interface.h: present but cannot be compiled" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h:     check for missing prerequisite headers?" >&5
+echo "$as_me: WARNING: stp/c_interface.h:     check for missing prerequisite headers?" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: see the Autoconf documentation" >&5
+echo "$as_me: WARNING: stp/c_interface.h: see the Autoconf documentation" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h:     section \"Present But Cannot Be Compiled\"" >&5
+echo "$as_me: WARNING: stp/c_interface.h:     section \"Present But Cannot Be Compiled\"" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&5
+echo "$as_me: WARNING: stp/c_interface.h: proceeding with the preprocessor's result" >&2;}
+    { echo "$as_me:$LINENO: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&5
+echo "$as_me: WARNING: stp/c_interface.h: in the future, the compiler will take precedence" >&2;}
+    ( cat <<\_ASBOX
+## ------------------------------------- ##
+## Report this to daniel@minormatter.com ##
+## ------------------------------------- ##
+_ASBOX
+     ) | sed "s/^/$as_me: WARNING:     /" >&2
+    ;;
+esac
+{ echo "$as_me:$LINENO: checking for stp/c_interface.h" >&5
+echo $ECHO_N "checking for stp/c_interface.h... $ECHO_C" >&6; }
+if test "${ac_cv_header_stp_c_interface_h+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+  ac_cv_header_stp_c_interface_h=$ac_header_preproc
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_header_stp_c_interface_h" >&5
+echo "${ECHO_T}$ac_cv_header_stp_c_interface_h" >&6; }
+
+fi
+if test $ac_cv_header_stp_c_interface_h = yes; then
+  :
+else
+
+         { { echo "$as_me:$LINENO: error: Unable to use stp/c_interface.h header" >&5
+echo "$as_me: error: Unable to use stp/c_interface.h header" >&2;}
+   { (exit 1); exit 1; }; }
+
+fi
+
+
+  CPPFLAGS="$old_CPPFLAGS"
+
+
+{ echo "$as_me:$LINENO: checking for vc_setInterfaceFlags in -lstp" >&5
+echo $ECHO_N "checking for vc_setInterfaceFlags in -lstp... $ECHO_C" >&6; }
+if test "${ac_cv_lib_stp_vc_setInterfaceFlags+set}" = set; then
+  echo $ECHO_N "(cached) $ECHO_C" >&6
+else
+  ac_check_lib_save_LIBS=$LIBS
+LIBS="-lstp -L$stp_root/lib $LIBS"
+cat >conftest.$ac_ext <<_ACEOF
+/* confdefs.h.  */
+_ACEOF
+cat confdefs.h >>conftest.$ac_ext
+cat >>conftest.$ac_ext <<_ACEOF
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char vc_setInterfaceFlags ();
+int
+main ()
+{
+return vc_setInterfaceFlags ();
+  ;
+  return 0;
+}
+_ACEOF
+rm -f conftest.$ac_objext conftest$ac_exeext
+if { (ac_try="$ac_link"
+case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_link") 2>conftest.er1
+  ac_status=$?
+  grep -v '^ *+' conftest.er1 >conftest.err
+  rm -f conftest.er1
+  cat conftest.err >&5
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); } &&
+	 { ac_try='test -z "$ac_cxx_werror_flag" || test ! -s conftest.err'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; } &&
+	 { ac_try='test -s conftest$ac_exeext'
+  { (case "(($ac_try" in
+  *\"* | *\`* | *\\*) ac_try_echo=\$ac_try;;
+  *) ac_try_echo=$ac_try;;
+esac
+eval "echo \"\$as_me:$LINENO: $ac_try_echo\"") >&5
+  (eval "$ac_try") 2>&5
+  ac_status=$?
+  echo "$as_me:$LINENO: \$? = $ac_status" >&5
+  (exit $ac_status); }; }; then
+  ac_cv_lib_stp_vc_setInterfaceFlags=yes
+else
+  echo "$as_me: failed program was:" >&5
+sed 's/^/| /' conftest.$ac_ext >&5
+
+	ac_cv_lib_stp_vc_setInterfaceFlags=no
+fi
+
+rm -f core conftest.err conftest.$ac_objext \
+      conftest$ac_exeext conftest.$ac_ext
+LIBS=$ac_check_lib_save_LIBS
+fi
+{ echo "$as_me:$LINENO: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
+echo "${ECHO_T}$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
+if test $ac_cv_lib_stp_vc_setInterfaceFlags = yes; then
+  cat >>confdefs.h <<_ACEOF
+#define HAVE_LIBSTP 1
+_ACEOF
+
+  LIBS="-lstp $LIBS"
+
+else
+
+         { { echo "$as_me:$LINENO: error: Unable to link with libstp" >&5
+echo "$as_me: error: Unable to link with libstp" >&2;}
+   { (exit 1); exit 1; }; }
+
+fi
+
+
+
+cat >>confdefs.h <<\_ACEOF
+#define HAVE_EXT_STP 1
+_ACEOF
+
+  ENABLE_EXT_STP=1
+
+  STP_ROOT=$stp_root
+
+fi
+
+
 ac_config_commands="$ac_config_commands Makefile"
 
 
@@ -5676,11 +5966,13 @@ CXX!$CXX$ac_delim
 CXXFLAGS!$CXXFLAGS$ac_delim
 ac_ct_CXX!$ac_ct_CXX$ac_delim
 CXXCPP!$CXXCPP$ac_delim
+ENABLE_EXT_STP!$ENABLE_EXT_STP$ac_delim
+STP_ROOT!$STP_ROOT$ac_delim
 LIBOBJS!$LIBOBJS$ac_delim
 LTLIBOBJS!$LTLIBOBJS$ac_delim
 _ACEOF
 
-  if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 76; then
+  if test `sed -n "s/.*$ac_delim\$/X/p" conf$$subs.sed | grep -c X` = 78; then
     break
   elif $ac_last_try; then
     { { echo "$as_me:$LINENO: error: could not make $CONFIG_STATUS" >&5
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 88f92d96..653b27a4 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -3,9 +3,15 @@
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
+/* Using external STP */
+#undef HAVE_EXT_STP
+
 /* 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 to 1 if you have the <memory.h> header file. */
 #undef HAVE_MEMORY_H
 
diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 30713253..4353857c 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -17,7 +17,11 @@
 #include <map>
 
 #define Expr VCExpr
+#ifdef HAVE_EXT_STP
+#include <stp/c_interface.h>
+#else
 #include "../../stp/c_interface/c_interface.h"
+#endif
 
 #if ENABLE_STPLOG == 1
 #include "stp/stplog.h"
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 1d13a11d..4059a82b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -453,6 +453,15 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
 
+#ifdef HAVE_EXT_STP
+  // In newer versions of STP, a memory management mechanism has been
+  // introduced that automatically invalidates certain C interface
+  // pointers at vc_Destroy time.  This caused double-free errors
+  // due to the ExprHandle destructor also attempting to invalidate
+  // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
+  // we restore the old behaviour.
+  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
+#endif
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index d9c417c1..21d84cbe 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -9,12 +9,21 @@
 
 LEVEL=../..
 TOOLNAME = kleaver
+
+include $(LEVEL)/Makefile.config
+
 STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a stp_sat.a \
 	stp_simplifier.a
 # FIXME: Ideally we wouldn't have any LLVM dependencies here, which
 # means kicking out klee's Support.
-USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a \
-	$(STP_LIBS)
+USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+ifeq ($(ENABLE_EXT_STP),0)
+  USEDLIBS += $(STP_LIBS)
+endif
 LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_EXT_STP),1)
+  LIBS += -lstp
+endif
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 72188b79..23c8f1d9 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -9,10 +9,19 @@
 
 LEVEL=../..
 TOOLNAME = klee
+
+include $(LEVEL)/Makefile.config
+
 STP_LIBS := stp_c_interface.a stp_AST.a stp_bitvec.a stp_constantbv.a stp_sat.a \
 	stp_simplifier.a
-USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a \
-	$(STP_LIBS)
+USEDLIBS = kleeCore.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+ifeq ($(ENABLE_EXT_STP),0)
+  USEDLIBS += $(STP_LIBS)
+endif
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
 include $(LEVEL)/Makefile.common
+
+ifeq ($(ENABLE_EXT_STP),1)
+  LIBS += -lstp
+endif
diff --git a/www/GetStarted.html b/www/GetStarted.html
index 20086600..84b36677 100644
--- a/www/GetStarted.html
+++ b/www/GetStarted.html
@@ -142,6 +142,40 @@ library.</p>
   </li>
 </ol>
 
+<h2 id="stp">Building KLEE with a more recent version of STP</h2>
+
+<p>If your benchmarks are running slowly or not terminating it may
+be worth trying a more recent version of KLEE's constraint solver
+<a href="http://sites.google.com/site/stpfastprover/">STP</a>,
+which offers performance improvements over the version supplied
+with KLEE.</p>
+
+<p>STP does not make frequent releases, and its Subversion repository
+is under constant development and may be unstable.  The instructions
+below are for a particular revision which is known to pass the KLEE
+test suite, but you can try a more recent revision (at your own risk)
+by changing or removing the <tt>-r</tt> argument to the <tt>svn
+co</tt> command.</p>
+
+<ol>
+  <li>Download and build STP.
+    <div class="instr">
+      $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp <br>
+      $ cd stp <br>
+      $ scripts/configure --with-prefix=<i>path/to/stp/inst</i> --with-cryptominisat2 <br>
+      $ make OPTIMIZE=-O2 CFLAGS_M32= install
+    </div>
+  </li>
+
+  <li>Configure KLEE:
+    <div class="instr">
+      $ ./configure --with-llvm=<i>path/to/llvm</i> --with-stp=<i>path/to/stp/inst</i>
+    </div>
+  </li>
+
+  <li>Rebuild KLEE.</li>
+</ol>
+
 </div>
 </body>
 </html>