# Interpolating Z3

A Craig interpolant is a formula that acts as an explanation for the unsatisfiability of a logical formula. Interpolating Z3 (iZ3) is a version of the Z3 theorem prover that can produce Craig interpolants from proofs. To be more specific, suppose “A” and “B” are logical formulas and we can prove “A implies B”. An interpolant for this implication is a formula `I `expressed only using symbols that are common to `A `and `B` that makes the following formulas valid:

• “A implies I”
• “I implies B”

The power of interpolants is that they put a proof in a syntactic form that allows it to be generalized. This ability can be applied, for example, to extract proofs about sequential circuits or programs from proofs about specific execution sequences, or to derive abstractions from counterexamples.

### Capabilities of iZ3

iZ3 can derive Craig interpolants from proofs in first-order logic, modulo certain theories, including:

• Integer linear arithmetic
• The theory of arrays

iZ3 handles quantified formulas, but does not always produce a quantifier-free interpolant when a quantifier-free interpolant exists. iZ3 can also produce sequence interpolants and tree interpolants, which are useful for program verification and constraint Horn clause (CHC) solving, as in the Duality CHC solver.