SMT-RAT: SAT-Modulo-Theories Real Arithmetic Toolbox

SMT-RAT is an open-source C++ toolbox for strategic and parallel SMT solving. It contains a collection of SMT compliant implementations for solving different logics, for example linear and nonlinear arithmetic over the reals or integers (QF_LRA, QF_LIA, QF_NRA, QF_NIA) as well as bitvectors (QF_BV).

• Documentation: https://github.com/smtrat/smtrat/wiki

Contact: Florian Corzilius, Gereon Kremer