Interpolating SMT-solver that can compute Craig interpolants for various theories
http://ultimate.informatik.uni-freiburg.de/smtinterpol/