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) 
  • QF_LIA — Theory of Linear Integer Arithmetics
  • QF_IDL 
  • QF_AX 

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 64 bits architectures.

OpenSMT2 participated in the SMTCOMP'14, SMTCOMP'15, and SMTCOMP16 and is consistently ranked among the top performing solvers in smt-comp and won the QF_LRA category in 2020.