Interpolating Z3

Interpolating Z3 uses Z3's proof generation capability to generate Craig interpolants in the first-order theory of uninterpreted functions, arrays and linear arithmetic.

Publications