Copyright 2019 Antti Hyvarinen [email protected]
Copyright 2009 Roberto Bruttomesso [email protected]

Project page: http://verify.inf.usi.ch/opensmt

OpenSMT is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

OpenSMT2 supports reading files in smtlib2 format and the theories QF_UF, QF_LRA, QF_RDL, and QF_LIA. The system also provides an api; the distribution includes a minimal example how to use the API.

To compile the system from the source code repository, you need a c++11 compliant compiler and the following libraries and headers installed:

• gmp
• readline

In addition the compilation system relies on cmake and the smtlib2 parser on flex and bison. To compile OpenSMT2, use the following command

$ mkdir build; cd build; cmake ..; make

If you have cmake version 3.11, the build system will construct unit tests. These are available through

$ ctest

OpenSMT supports a range of interpolation options for propositional logic, linear real arithmetic, and uninterpreted functions with equality. To enable interpolation code the compilation needs to be configured by enabling PRODUCE_PROOF in the cmake configuration file CMakeCache.txt produced by cmake in your build directory.

If you have questions please mail them to me at [email protected], or to the discussion forum!