ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
60 stars 17 forks source link

ERROR - The proof did not yield a contradiction #148

Closed rodrigo7491 closed 4 months ago

rodrigo7491 commented 4 months ago

For the attached file (see test.zip) SMTInterpol produces a proof that is classified as invalid when given to its checker. The output of the check is as below.

WARN - Could not find pivot + (or (exists ((x!3 Int)) (and (not (<= (+ x!3 1) 0)) (not (<= (+ (* (- 1) x!3) 1) 0)))) (= A 1)) in [+ (exists ((x!3 Int)) (and (not (<= (+ x!3 1) 0)) (not (<= (+ (* (- 1) x!3) 1) 0)))), + (= A 1)]
ERROR - The proof did not yield a contradiction but [+ (exists ((x!3 Int)) (and (not (<= (+ x!3 1) 0)) (not (<= (+ (* (- 1) x!3) 1) 0)))), + (= A 1)]
invalid

Solver command: java -jar smtinterpol-2.5-1256-g55d6ba76.jar test.smt2 Checker command: java -cp smtinterpol-2.5-1256-g55d6ba76.jar de.uni_freiburg.informatik.ultimate.smtinterpol.proof.checker.Main test.smt2 test.proof

I am using smtinterpol-2.5-1256-g55d6ba76 on Linux Mint 21.2.

jhoenicke commented 4 months ago

Thanks for the report. The proof is only slightly wrong: the statement is true and removing a single wrong resolution step fixes the problem. There is a problem with the proof of an instantiation clause.

It has something to do with the intermediate proof representation of instantiation lemmas and the fact that we sometimes create auxiliary literals for (or ...) terms. In this proof a lemma should proof the unit clause with the literal (or A B), but the proof simplifier assumes that it should proof the clause A,B instead.

The latest master should fix this problem.