search

ultimate-pa / smtinterpol

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

AssertionError with check-sat-assuming #29

Open mskamp opened 7 years ago

mskamp commented 7 years ago

Using the following (already reduced) test file, SMTInterpol 2.1-335-g4c543a5 produces an AssertionError:

(set-logic QF_UFLIA)
(declare-fun g0 () Bool)
(declare-fun a (Int Int) Bool)
(define-fun b ((t Int)) Int (+ (+ 0 (ite (a 0 t) 1 0)) (ite (a 2 t) 1 0)))
(assert (let ((.cse0 (b 2))) (< .cse0 1)))
(check-sat-assuming (g0))

When executing java -ea -jar smtinterpol-2.1-335-g4c543a5.jar < test.smt2 the solver outputs the following lines:

success
success
success
success
INFO - Sharing term: 2
INFO - Sharing term: 0
success
Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getLevel0(DPLLEngine.java:1556)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.level0resolve(DPLLEngine.java:868)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:747)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:858)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1215)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:115)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:528)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2295)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1146)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:147)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:125)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:37)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)

As it seems to me, check-sat-assuming is the culprit here. Replacing (check-sat-assuming (g0)) with (assert g0) (check-sat) produces the correct result.

jhoenicke commented 7 years ago

check-sat-assuming is not very well tested and still buggy. The fix is not trivial, since the interactions with the DPLL engine are very tricky. I will probably change it soon to execute the sequence push, assert, check-sat, pop internally.

kfriedberger commented 3 years ago

Any news on this bug? It still appears in SMTInterpol 2.5-732-gd208e931.