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 OpenSMT2 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.