Ivannikov Institute for System Programming of the RAS

Instantiation-Based Interpolation for Quantified Formulae in CSIsat.


Mutilin V., Mandrykin M.


The paper describes an implementation of instantiation-based interpolation for quantified formulae in modified CSIsat tool. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. We propose in this paper using external SMT-solver CVC3 for quantified expressions instantiation, then we describe how we modified CSIsat and CVC3 tools in order to support quantified formulae interpolation. We also present results of benchmarking the modified CSIsat tool on SMTLIB test set as well as on our specially generated interpolation tasks.

Full text of the paper in pdf


interpolation, Craig interpolant, quantifiers, instantiation, solver, axioms.


Proceedings of the 6th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE), pp. 85-93.

DOI: 10.15514/SYRCOSE-2012-6-12

Research Group

All publications during 2012 All publications