Unknown axiom required for verification, but not present in instantiation graph or unsat core

[kiranandcode]

I have an SMT query with an axiom that is required for verification however does not seem to show up in the unsat core, in the instantiation graph or even in the proof of correctness.

I have attached the query and the trace file from running with proof=true trace=true. These have all been run on the latest version of Z3 (4.13.0).

When passing the trace file to the axiom profiler, this is the resulting instantiation graph --- highlighted, the two green instantiations do not seem to result in any instantiations of axioms in the unsat core however removing them causes verification to fail.

The smt query: query-smt.txt

The trace file: z3.log

The output when running Z3 on this file:

unsat
(:rlimit 3022)
(axiom$$491389 axiom$$491332 axiom$$490811)

The necessary axiom is at line 3638, and has quantifier id |originalbpl.183:18-key|

(assert (! using-axiom-487317 :named axiom$$487317))
(assert  (=> using-axiom-487317
             (forall ((x@@51 T@Seq_165642))
                     (! (= ($Unbox_165645 ($Box_165660 x@@51)) x@@51)
                        :qid |originalbpl.183:18-key|
                        :skolemid |25|
                        :pattern ( ($Box_165660 x@@51))
                        ))))

Z3 version

Z3 version 4.13.0 - 64 bit

[kiranandcode]

The generated proof (see below) also doesn't seem to make use of the axiom either

[kiranandcode]

I'm guessing it might be due to https://z3prover.github.io/papers/z3internals.html#sec-tactic-elim-predicates

is there a way to disable this?

[kiranandcode]

Actually looking into this, I realise this same issue occurs back in 4.8.7 before elim predicates was even enabled so I don't think that's the cause

[kiranandcode]

If I reverse the order of the equality, it shows up in the unsat core:

(assert (! using-axiom-487317 :named axiom$$487317))
(assert  (=> using-axiom-487317
             (forall ((x@@51 T@Seq_165642))
                     (! (= x@@51 ($Unbox_165645 ($Box_165660 x@@51)))
                        :qid |originalbpl.183:18-key|
                        :pattern ( ($Box_165660 x@@51))
                        ))))

[NikolajBjorner]

@alexanderjsummers @jonasalaif - I am not sure if this is whether all dependencies are available or whether it is a blame in the inferences. Looking at smt_quantifier.cpp, the dependencies are logged using two mechanisms: explain the roots of each binding, and explain a set of equalities that were used within mam.cpp. So there are several moving parts that are supposed to synchronize and produce the relevant information.

On a side-node: enodes have a tagging mechanism (mark1, mark2), so the hash table https://github.com/Z3Prover/z3/blob/ea417bbf926abf40b28b79c6381dff91d7e92b07/src/smt/smt_quantifier.cpp#L252 could be dispensed with. Of course, the enodes cannot be already marked by some other context.

[NikolajBjorner]

Trying this:

• z3 query-smt.txt /v:2 smt.relevancy=0 sat.smt=true
• remove the line that sets mbqi to false.
• ;(assert (! using-axiom-487317 :named axiom$$487317))

It produces unsat with the small core.

[alexanderjsummers]

@NikolajBjorner thanks for the comment. Unfortunately I'm not very familiar with the mechanism on the Z3 side (I wasn't aware that it's as heavyweight as this for equalities), but I know the logic in the (older) Axiom Profiler that seems to mimic a similar idea after reading the corresponding logs. Do you mean that there is a more direct way to recover the relevant set of equalities for a match? If I understand correctly, it does seem as though the hashtable is trying to build some approximation of the egraph information, which is a little awkward.

[alexanderjsummers]

However, if I understand the overall issue correctly, the necessary quantifier doesn't show up (always) in the unsat core; I guess that means there is an underlying problem independent of how the logs are being constructed. I suppose what we are (not) seeing in the logged information might be symptomatic of some missing dependency in Z3's calculations?