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
- Kenneth L. McMillan, Interpolants from Z3 proofs, in Formal Methods in Computer-Aided Design, 30 October 2011
