About SMTInterpol

SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. The solver is developed at the Chair of Software Engineering at the University of Freiburg.
The solver is written in Java and can be used on any operating system that supports Java Version 8 or above.
The solver reads input in SMTLIB Version 2.6 format.

Status

The current version of SMTInterpol supports the combination of the theories of uninterpreted functions, linear real arithmetic, linear integer arithmetic, arrays including constant arrays, and datatypes.
SMTInterpol supports quantifiers for all supported theories except for datatypes, and it supports interpolation for the quantifier-free fragments of all supported theories except datatypes.

System Requirements

SMTInterpol needs a Java 8 JRE or above. No special hardware is necessary but depending on the input problem, a fast CPU and a good amount of RAM might be useful.

Current Team

SMTInterpol is developed by Jochen Hoenicke in the context of the project "Quantified Formulas in Interpolating SMT Solvers" and by Elisabeth Henkel and Tanja Schindler. If you have any questions, suggestions, or if you want to contribute, feel free to contact us.

Other contributors

NameMain contribution
Max BarthTheory solver for bitvectors
Daniel BlankProof translation to SMTCoq
Jürgen ChristMajor parts of SMTInterpol
Leonard FichtnerUnsat core enumeration and heuristics
Joanna GreulichParser for datatypes
Moritz MohrTheory solver for datatypes
Alexander NutzTheory solver for EPR
Markus PomrehnFine-grained rewrite proofs
Andrea QosjaWeb interface
Pascal RaiolaTrigger compiler
Daniel Dietsch, Matthias HeizmannSMT-LIB libraries

Bug Reports

Please use our github page to report bugs.

License

SMTInterpol is distributed under LGPL Version 3.

SMTInterpol in Action

SMTInterpol participates regularly in the SMT-COMP. See this page or the news page for further details.