As a part of research on decision procedures, our Lab develops a tool, OpenSMT, that is used as a framework to perform all our experiments.
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand and use as a computational engine for formal verification. OpenSMT is built on top of MiniSAT.
The git repository for OpenSMT is available at
git clone https://github.com/usi-verification-and-security/opensmt.git
The new OpenSMT2 is currently under active development, built on the solid foundations of the previous OpenSMT generations but providing native support for the SMTLIB version 2 and more efficient implementation for most internal data structures. OpenSMT2 is released under the MIT license. For now, old OpenSMT1 still provides support for a wider variety of theories and is released under the General Public Licence version 3 license.