Can Z3 generate Craig interpolants (at least for propositional logic ?). I have not found it in the documentation of Z3.
No, Z3 does not support Craig interpolants, but it generates proofs. The interpolants can be extracted from the proofs. Ken Mcmillan is developing an interpolant generator on top of Z3 using this approach.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With