Compilation

We assume you have already cloned OpenSMT's repository using git:

 $ git clone https://github.com/usi-verification-and-security/opensmt.git

OpenSMT2 uses CMake for the build process. Moreover, a C++ compiler supporting C++11 standard is needed for compilation.

Additional libraries that are expected to be found on your system are:

  • readline (for ubuntu: sudo apt-get install libreadline-dev)
  • gmp (for ubuntu: sudo apt-get install libgmp-dev)
  • bison (for ubuntu: sudo apt-get install bison)
  • flex (for ubuntu: sudo apt-get install flex)

After cd to the top-level OpenSMT directory, follow these steps to compile OpenSMT:

Create your build directory and enter it

 $ mkdir build && cd build

Run CMake with the path to the top-level CMakeLists.txt, optionally specified your build type, e.g.:

 $ cmake -DCMAKE_BUILD_TYPE=Release ..

If proof producing capabilities are required (e.g. for interpolation) enable the option PRODUCE_PROOF

 $ cmake -DCMAKE_BUILD_TYPE=Release -DPRODUCE_PROOF=ON ..

If cmake configuration step was successful, you can compile using make

 $ make

Now opensmt executable is located in <opensmt_root>/build/src/bin folder. You can also install the executable on your system (possibly with sudo)

 $ <sudo> make install

 

 

Building older version of OpenSMT (with old build system)

Prerequisite libraries:

OpenSMT2 depends on the following libraries:

  • zlib
  • gmp
  • gmpxx
  • readline
  • flex

Guideline to install the requirements:

sudo apt-get update

sudo apt-get install gcc-6

sudo apt-get install g++-6

sudo rm /usr/bin/cpp /usr/bin/gcc /usr/bin/g++

sudo ln -s /usr/bin/cpp-6 /usr/bin/cpp

sudo ln -s /usr/bin/gcc-6 /usr/bin/gcc

sudo ln -s /usr/bin/g++-6 /usr/bin/g++

sudo apt-get install libtool

sudo apt-get install bison flex

sudo apt-get install autoconf

sudo apt-get install git-all

 

Guideline to Install GMP:

wget ftp://ftp.gmplib.org/pub/gmp/gmp-6.1.2.tar.xz

tar Jxvf gmp-6.1.2.tar.xz

cd gmp-6.1.2

./configure --enable-cxx

make

make check

sudo make install
 

Compilation with Makefile (for normal usage, not theory or summary refinement)

To compile OpenSMT2, first download it via:

$ git clone https://scm.ti-edu.ch/repogit/opensmt2.git

Enter the opsntm2 folder and run the configure script:

$ cd opensmt2
$ autoreconf --force --install

If you want to enable interpolation in OpenSMT2, configure with the following parameter:

$ ./configure --enable-proof

but if you need opensmt to use theory refinement algorithm, please configure it without any parameter:

$ ./configure

 

Then run make and install.

$ make
$ sudo make install

 

** If you need any assistance, please contact us **

antti.hyvarinen[at]gmail.com Or sepideh.a65[at]gmail.com