How to compile SMTS?


SMTS: a framework for distributed SMT and PDR, supporting lemma sharing and partitioning

$ git clone



1) Download and install the dependencies

  • PDR: Z3-Spacer supporting lemma sharing

$ git clone -b p3
$ mkdir build; cd build; cmake ..; make -j8 install
  • SMT: OpenSMT2

$ git clone
$ autoreconf --force --install
$ ./configure --enable-library
$ make -j8 install


2) Compile SMTS

$ cd smts
$ mkdir build; cd build; cmake ..; make -j8

Note 1: you can disable either SMT or PDR support by commenting the respective lines in: ./src/client/CMakeLists.txt

Note 2: If SMTS cmake script can't find lib or headers (e.g. you installed in non-standard folders), then use:

$ cmake -DOPENSMT2_DIR=<install_dir> -DZ3SPACER_DIR=<install_dir> ..


3) Configure SMTS

Copy the default "read-only" configuration file:

$ cp ./server/config/ ./server/config/

Note 3: If SMTS is not compiled in ./build then change ./server/config/ variable build_path accordingly

Note 4: SMTS loads ./server/config/ automatically. However using -c, you can specify other configuration files that (partially) override options. 


4) Try SMTS locally

These might help:

$ ./ --help
$ ./ --help


The following command executes 4 OpenSMT processes with lemma sharing and enables the GUI:

$ ./ -g -d test.db -o4 -l

The following command executes 4 Z3-Spacer processes with lemma sharing + storage and enables the GUI:

$ ./ -g -d test.db -z4 -l -D

In both cases benchmarks are provided using:

$ ./ 3000 <benchmark-path>

To analyze a given database use:

$ ./ -g <db-path>

To see the GUI open the browser at


Other links:


P3 full experimental results from FMCAD 2017