Counterexample output of Z3

Question

When a formula in Z3 is unsat and (get-proof) is specified there is an output which I don't find any information about what it is. Where can I find any documentation about that?

Seems to me quite unreadable, is there possibly any tool that takes this as an input?

Cheers, Matt

Answer 1

The "proofs" produced by Z3 are not for human consumption. An outdated version of the format is described in the paper: Proofs and Refutations, and Z3. The z3_api.h file has a long description of each one of the proof rules. The proof rule identifiers start with Z3_OP_PR. I am aware of two applications that use the Z3 proof objects. The following papers contain a lot of examples, and describe how the proof objects can be used.

1. Isabelle Interactive Theorem Prover: Z3 proofs are reconstructed inside of Isabelle using a trusted core. You can find several papers describing this work and the Z3 proof format at Sascha Bohme's homepage

2. Generation of interpolants

   As pad said, unsat-cores are much simpler to use.