OpenSMT is an open-source SMT solver developed at the University of Lugano. The new version, OpenSMT2, is a newcomer to the family of SMT solvers, even though it owes much of its performance to the previous versions of the solver. Unlike the old version, the new OpenSMT2 is released under the MIT license.
OpenSMT2 now has a new term handling functionality that allows a complete separation between theory specific parts and the structure of the problem, while still maintaining all the optimizations present in the previous version. The support for the smtlib2 standard has been built in to the solver in a way that in future allows expanding the range of supported theories in a natural way that previously was not possible.
At the moment the solver implements the theory of quantifier-free uninterpreted functions with equalities (QF_UF). The implementation handles the memory used by the critical data structures in a custom way, giving an average of 15% boost to the wall-clock performance compared to its predecessor in the operations related to these data structures.
The solver has been thoroughly tested for both performance and correctness. The solver competed in the SMT-COMP 2014, and while the version submitted to the competition still suffered from certain inefficiencies, such as a naive implementation of theory propagation, it is already in many respects comparable to the state-of-the-art in its field, placing it in the mid-range in the QF_UF category.