-
Notifications
You must be signed in to change notification settings - Fork 1
System SMTInterpol
The main developer of SMTInterpol is Jochen Hoenicke. Other major parts have been written by Jürgen Christ, Elisabeth Henkel, Alexander Nutz, and Tanja Schindler. See the official webpage for a list of contributors.
SMTInterpol is an interpolating SMT solver. The solver supports all combinations of the theories of uninterpreted functions, linear real arithmetic, linear integer arithmetic, mixed linear real and integer arithmetic, arrays including constant arrays, and datatypes. It also supports their quantified fragments. In addition to satisfiability checks, SMTInterpol can provide interpolants, unsat cores, proofs, and models where applicable.
SMTInterpol has mostly been developed in the Software Engineering group at the University of Freiburg.
- Proving
- Model finding
The input format is SMT-LIB 2.6. Additional non-standard commands, in particular for interpolation, are described on the webpage.
SMTInterpol produces output according to the SMT-LIB reporting standard.
SMTInterpol outputs proofs in the RESOLUTE format, a simple resolution-based format.
https://ultimate.informatik.uni-freiburg.de/smtinterpol/
SMTInterpol is tightly integrated in the open-source model checking framework Ultimate.
SMTInterpol regularly participates in the SMT-COMP.
SMTInterpol is written in Java, and only requires Java 8 JRE or higher to run. It is open-source and licensed under LGPL version 3. The code is available on GitHub.
Maintained
Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An Interpolating SMT Solver. In SPIN 2012. DOI: https://doi.org/10.1007/978-3-642-31759-0_19
For a list of publications related to SMTInterpol, see the official webpage.
A proof checker for SMTInterpol's proof format is available.