an Interpolating SMT Solver
SMTInterpol at SMTCOMP 2014
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.
Awards for SMTInterpol during VSL 2014The goedel medal
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.
New preview release
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.
New minor release
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.
New release
A new release is available. This release fixes a bug in the tree interpolation engine and provides SMTLIB 2 compliant models for IRA logics.
New bugfix release
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.
SMT Competition 2012
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.
Proof Transformations
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
License Change
On popular demand we changed the license of SMTInterpol from GPL to LGPL.
SMT Competition 2011
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.

Last modified: Wed Sep 7 16:11:56 CEST 2016   Valid XHTML 1.0 TransitionalValid CSS!