**Overview**

OpenSMT is a small, efficient and open-source SMT-Solver, currently released under the BSD-licensed.

The main motivations of OpenSMT are:

- to promote the use of SMT-Solvers in combination with other verification tools
- to provide a level of detail of decision procedures that goes beyond the scientific publication
- to promote the development of efficient SMT-Solvers by providing a simple infrastructure for helping non-experts to develop theory-solvers without having to start from scratch

OpenSMT includes a parser for SMT-LIB language, a state-of-the-art SAT-Solver, and a clean interface for plugging in new theory-solvers; a template (empty) theory-solver is provided, to facilitate the development of solvers for other logics.

OpenSMT currently supports the following logics: QF_UF, QF_LIA, QF_LRA, QF_IDL, QF_RDL, QF_AX, QF_UFLIA, QF_UFLRA.

**Implementation Details**

OpenSMT is written in C++. It is based on MiniSAT 2.0 [2]. We tried to avoid modifications of its code as much as possible. Any added or modified line in the code is explicitly indicated.

A feature of OpenSMT is to provide an automatic mechanism to compute* reasons* for theory-deductions by means of the consistency check algorithm. This makes it easier the implementation of a new solver, as the solver is required just to *detect* deduction without having to provide an immediate explanation for them, and without storing any additional information. This mechanism enables the possibility of performing theory-propagation for inherently complex theories such as bit-vectors.

OpenSMT implements a preliminary preprocessor for SMT arithmetic formulae based on [5].

The congruence closure algorithm implemented is the same as the one used in Simplify [1], however, we rely on the algorithm of [3] for retrieving explanations: this can be done by storing the necessary information for retrieving the conflict inside the data structures for term-representation described in [1].

The difference logic solver is based on [6] and it works on integers. QF_RDL benchmarks are translated into the equisatisfiable QF_IDL version at preprocessing time. The solver for QF_LRA is based on [7]. Every arithmetic solver supports infinite precision arithmetic, ultimately based on GMP [8]. The solver for QF_BV is ultimately based on bit-blasting. It also embeds the decision procedure described in [9].