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