Z3 disable assertion simplification for proofs

Question

Is there any way to disable simplification/rewriting of assertions in Z3 (version 4.8.8)?

I am currently working on proof replay of Z3 proofs within KeY (https://www.key-project.org). However, to be able to replay Z3's "asserted" rule, I need the exact assertion as specified in the SMT-LIB input to Z3, not a simplified version of it.

As an extreme example of what could happen, consider this SMT-LIB input:

(set-option :produce-proofs true)

(assert
  (not
    (forall ((y Int))
      (exists ((x Int))
        (= x (+ y 1))
      )
    )
  )
)
(check-sat)
(get-proof)

Running Z3 4.8.8 leads to the following output:

unsat
((proof
(asserted false)))

Obviously, the assertion has been simplified, which makes the proof not really helpful. Is there any way to completely disable this simplification (and thus get a "real" proof from Z3, which I can replay in our tool)?

Answer 1

You might be better served if you use a more recent version of z3. For instance, given your example, a recently compiled-from-github-master version produces:

((proof
(let (($x88 (not true)))
 (let (($x48 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ 1 y)) :qid k!8))
  :qid k!9))
 ))
 (let (($x54 (not $x48)))
 (let ((@x36 (rewrite (= $x54 $x54))))
 (let (($x30 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ y 1)) :qid k!8))
  :qid k!9))
 ))
 (let (($x31 (not $x30)))
 (let ((@x32 (asserted $x31)))
 (let ((@x45 (mp (mp (mp @x32 (rewrite (= $x31 $x54)) $x54) @x36 $x54) @x36 $x54)))
 (let ((@x53 (mp (mp (mp @x45 @x36 $x54) @x36 $x54) (rewrite (= $x54 $x88)) $x88)))
 (mp @x53 (rewrite (= $x88 false)) false))))))))))))

The format remains undocumented, and in general it will be really hard for z3 to produce granular proofs in the presence of quantifiers. A direct quote from: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-proofs says:

The granularity of proof objects is on a best-effort basis. Proofs for the SMT Core, are relatively fined-grained, while proofs for procedures that perform quantifier elimination, for instance QSAT described in Section 6.4, are exposed as big opaque steps.