an Interpolating SMT Solver

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.5 format.


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

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.


SMTInterpol is developed by Jochen Hoenicke and Tanja Schindler in the context of the SIGSMCAP (SMT-based Interpolant Generation for Software ModelChecking of Array Programs) project, and by Alexander Nutz. If you have any questions, suggestions, or if you want to contribute, feel free to contact us. Previous contributors include J├╝rgen Christ.

Bug Reports

Please use our github page to report bugs.


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.

Last modified: Sat May 9 15:30:42 CEST 2020   Valid XHTML 1.0 TransitionalValid CSS!