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

1 files changed, 34 insertions, 0 deletions

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>