OpenSMT1 is no longer actively developed. This page is for archival purposes.

OpenSMT1 is the old version of our OpenSMT tool.

OpenSMT1 supports the following theories:

• QF_UF — Theory of Equality and Uninterpreted Functions
• QF_IDL — Theory of Differences on the Integers
• QF_RDL — Theory of Differences on the Rationals
• QF_LRA — Theory of Linear Arithmetic on the Rationals
• QF_BV — Theory of Fixed-Width Bit Vectors
• QF_UFIDL — Theory combination of Uninterpreted Functions and Differences on the Integers
• QF_UFLRA — Theory combination of Uninterpreted Functions and Linear Arithmetic on the Rationals

OpenSMT1 is released under the GNU General Public Licence version 3.

Code is available via SVN here. It compiles on 64 bits architectures.

We encourage other researchers to build their algorithms for SMT solving in the OpenSMT framework. For that, we dramatically simplified the process of building/customizing the solver.

OpenSMT1 participated in the SMTCOMP'08 and SMTCOMP'09. Although not yet as fast as other industrial systems, OpenSMT was at the time the fastest open-source SMT Solver for QF_UF, QF_IDL, QF_RDL, QF_LRA theories.

A general system description can be found here.