Interpolating provers have a number of applications in formal

verification, including abstraction refinement and invariant

generation. It has proved difficult, however, to construct efficient

interpolating provers for rich theories. We consider the problem of

deriving interpolants from proofs generated by the highly efficient

SMT solver Z3 in the quantified theory of arrays, uninterpreted

function symbols and linear integer arithmetic (AUFLIA) a theory

that is commonly used in program verification. We do not directly

interpolate the proofs from Z3. Rather, we divide them into small

lemmas that can be handled by a secondary interpolating prover for a

restricted theory. We show experimentally that the overhead of this

secondary prover is negligible. Moreover, the efficiency of Z3 makes

it possible to handle problems that are beyond the reach of existing

interpolating provers, as we demonstrate using benchmarks derived

from bounded verification of sequential and concurrent programs.

PDF file

In  Formal Methods in Computer-Aided Design

Details