STP is the recommended solver in KLEE. The instructions below are for release 2.3.3. If you would like to use the upstream version, do not perform the checkout command git checkout tags/2.3.3 in the instructions below.

STP has a few external dependencies that are first listed here as an install command for Ubuntu 18.04:

sudo apt-get install cmake bison flex libboost-all-dev python perl zlib1g-dev minisat

Under macOS, you can run:

brew install cmake bison flex python perl

If your distribution does not offer MiniSAT, you need to install it manually:

$ git clone https://github.com/stp/minisat.git
$ cd minisat
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/usr/local/ ../
$ sudo make install

To install STP, run:

$ git clone https://github.com/stp/stp.git
$ cd stp
$ git checkout tags/2.3.3
$ mkdir build
$ cd build
$ cmake ..
$ make
$ sudo make install

Before running KLEE with STP on larger benchmarks, it is essential to set the size of the stack to a very large value:

$ ulimit -s unlimited

On macOS, you’ll likely have to run:

$ ulimit -s 65532

You can make this persistent by editing the /etc/security/limits.conf file or adding the ulimit command into e.g, .bashrc.