SMTInterpol now has a web interface. More precisely, our web interface runs SMTInterpol in the browser. It was created by Andrea Qosja using TeaVM to compile SMTInterpol into JavaScript.

We participated in the SMT-COMP 2021. In the single-query track we won the division "Quantifier-free Equality with Linear Arithmetic". In the incremental track we won "Quantifier-free Nonlinear Integer Arithmetic" and "Quantifier-free Equality with Nonlinear Arithmetic". We scored the second place in the biggest lead ranking for the incremental track.

We participated in the SMTCOMP 2018 which was part of the FLoC Olympic Games in Oxford. SMTInterpol won the unsat core track for quantifier-free linear integer arithmetic and real arithmetic (QF_LIA and QF_LRA) and made it to the third place in the overall evaluation.

SMTInterpol now supports interpolation in the quantifier-free logic of arrays.

We released version 2.5 of SMTInterpol. This release has full support for the quantifier-free fragment for arrays. Although this theory have been supported in the solver for a while, the new release also supports generation of interpolants for this theory. We also updated the parser to support SMTLIB version 2.5.

We participated in the SMTCOMP 2014 which was part of the Vienna Summer of Logic Olympic Games. The primary new feature was our array solver which performed really good. We were awarded with the Gödel medal for the second place according to the multi-division error-free scoring. Furthermore, David Cok - the lead organizer of the competition - awarded us with a beautiful "big A" also known as a universal quantifier when put in correct position. We thank all the supporters that helped to improve SMTInterpol and, of course, the organizers of the competition and the VSL olympic games for these nice awards.

The scoring system that was applied this year penalized errors in a draconic way. This quasi led to the disqualification of the main competitors CVC4 and Yices. Also Z3 and MathSAT were not competing this year. Therefore the second place should be taken with a grain of salt.

A preview to release 2.2 of SMTInterpol is available. This release contains a new array decision procedure which is designed to enable quantifier-free interpolation. The interpolation procedure however is not yet implemented. Additionally we changed the model generation such that we now produce anonymous terms of the form (as @0 S) for a sort S. The array model basically are a difference map to an array (as @0 (Array TI TE)) that contains at every index the value (as @0 TE). Note that in the current version of our array solver the index type Bool is not supported.

Release 2.1 of SMTInterpol is available. Among some bug fixes this release includes support for user cancellation requests. While SMTInterpol is performing a satisfiability check it now regularly polls a cancellation request that can be configured via the API.

A new release is available. This release fixes a bug in the tree interpolation engine and provides SMTLIB 2 compliant models for IRA logics.

A new release of SMTInterpol is available. It now allows users to define functions that take arguments in QF_LIA and QF_LRA. Thanks to Hans-Martin Adorf for reporting this bug.

SMTInterpol participates in the SMT-COMP 2012 in the main, application, unsat-core, and in the demonstration track. A slightly newer version of SMTInterpol is available from the download page.

The latest version of SMTInterpol incorporates the proof tree transformation techniques presented by Fontaine et. al. in their paper Compression of Propositional Resolution Proofs via Partial Regularization". The option :proof-transformation can be used to activate one of the algorithms presented in this paper. Possible values are:

Value	Description
NONE	No transformation (default)
LU	Lower all unit resolutions such that every unit is resolved only once in the whole proof tree.
RPI	Recycle pivots by partial regularization.
LURPI	First lower units, then recycle pivots.
RPILU	First recycle pivots, then lower units

On popular demand we changed the license of SMTInterpol from GPL to LGPL.

A pre-release version of SMTInterpol 2.0 participated in the SMT-COMP 2011 in the main and in the application track. See these pages for further details. This was the first time SMTInterpol participated in the competition. It showed its strength in the divisions QF_UFLRA and QF_UFLIA where it could solve as many instances as the winner of this division in the main track.