OpenSMT

 

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 (http://minisat.se).

There are two versions of OpenSMT.  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 a support for a wider variety of theories and is released under the General Public Licence version 3 license.