OpenSMT1

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

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 - see "Build your solver" tutorial.

OpenSMT is currently released under the GNU General Public Licence version 3. Code is available via SVN at http://code.google.com/p/opensmt/. It compiles on 32 and 64 bits architectures.

OpenSMT participated 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.