OpenSMT2 supports the following theories:

  • QF_UF — Theory of Equality and Uninterpreted Functionsions
  • QF_LRA — Theory of Linear Real Arithmetics
  • QF_RDL — Theory of difference in Linear Real Arithmetics (a subset of QF_LRA) 

We support reading the smtlib2 format, and provide three library interfaces for C, C++ and python for communicating with the solver.

We encourage other researchers to build their algorithms for SMT solving in the OpenSMT2 framework.

OpenSMT2 is released under the MIT license. Code is available here. It compiles on 32 and 64 bits architectures.

OpenSMT2 participated the SMTCOMP'14, SMTCOMP'15, and SMTCOMP16.  Although the competition version was still lacking in performance, the solver finished in the mid-range in the QF_UF category.