Interpolation and Model Checking for Nonlinear Arithmetic

Dejan Jovanović, Bruno Dutertre

We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving…