Abstract. Craig interpolation is an active research topic and has become a powerful technique in verification. We present SMTInterpol, an interpolating SMT solver for the quantifier-free fragment of the combination of the theory of uninterpreted functions and the theory of linear arithmetic over integers and reals. SMTInterpol is SMTLIB 2 compliant and available under an open source software license (LGPL v3).