SMTInterpol
SMTInterpol is an SMT-Solver which can compute Craig interpolants for the quantifier free combined theory of uninterpreted functions, linear arithmetic over rationals and integers, and arrays.
The solver is developed by Jochen Hoenicke1 and Tanja Schindler2. Previous contributors include Jürgen Christ3 and Alexander Nutz4.
The website of SMTInterpol is https://ultimate.informatik.uni-freiburg.de/smtinterpol/5.
