Failed resolution check

[BrunoDutertre]

I'm getting some errors again related to failed resolution steps. Here's a reduced example.

(set-logic QF_UF)
(declare-sort I 0)
(declare-fun o (I I) I)
(declare-fun e () I)
(declare-fun e3 () I)
(declare-fun e0 () I)
(assert (and (= (o e0 e3) (o e0 e)) (or (= e (o e0 e3)) (= e (o e0 e)))))
(assert (not (= e (o e0 e3))))
(check-sat)

I got a proof from cvc5 as follows:

cvc5 --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --proof-granularity=theory-rewrite iso_icl083_reduced.smt2

Then checking the proof fails:

carcara check tmp.prf iso_icl083_reduced.smt2 --skip-unknown-rules
[ERROR] checking failed on step 't38' with rule 'resolution': pivot was not eliminated: '(not (= e (o e0 e3)))'
invalid

Here's the relevant proof fragment:

(assume a1 (not (= e (o e0 e3))))
(step t37 (cl (or (= e (o e0 e3)) (= e (o e0 e)))) :rule and :premises (a0))
(step t38 (cl (= e (o e0 e))) :rule resolution :premises (t37 a1))

Could be one of these confusing 'or' vs clause thing (a cvc5 bug), but I'm reporting it here for confirmation.

[bpandreotti]

Yeah, this looks to me like a cvc5 bug, similar to the other issue. Here, step t37 concludes a unit clause with an or term. If it instead was a clause with the two or arguments ((cl (= e (o e0 e3)) (= e (o e0 e)))) the proof would check without errors.

What version of cvc5 are you using? I can't reproduce this on the latest version (https://github.com/cvc5/cvc5/commit/6a0abb70032db7bd747724477ca63372e7c801eb), cvc5 adds an or step after t37:

(assume a1 (not (= e (o e0 e3))))
(step t37 (cl (or (= e (o e0 e3)) (= e (o e0 e)))) :rule and :premises (a0))
(step t38 (cl (= e (o e0 e3)) (= e (o e0 e))) :rule or :premises (t37))
(step t39 (cl (= e (o e0 e))) :rule resolution :premises (t38 a1))

[BrunoDutertre]

I'm on commit d575cab3a2.

[BrunoDutertre]

It's not fixed in https://github.com/cvc5/cvc5/commit/6a0abb70032db7bd747724477ca63372e7c801eb. The same thing happens on other examples.

[HanielB]

Hi Bruno. In cvc5/cvc5@d575cab3a2 the fix I had done for this issue had not been merged into main yet. As of cvc5/cvc5@6a0abb7. I cannot reproduce with it this issue. Do you have other examples in which this is happening?

[BrunoDutertre]

Yes, I have a few. ddSMT has been crunching on one of them for 5 days.

[HanielB]

I see (now I'm a bit scared hehe). Can you please open an issue in the cvc5 repo when you have a benchmark you can share? I'll close the issue here since it's not a problem with Carcarca.

[BrunoDutertre]

It could be a different issue. But the symptom is the same 'pivot was not eliminated`. I'll post to cvc5 when ddSMT is done.

[HanielB]

Great, thanks!