search

ultimate-pa / smtinterpol

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

NullPointerException at DPLLEngine.java:782 #137

Open daniel-larraz opened 2 years ago

daniel-larraz commented 2 years ago

Running SMTInterpol on this SMT script (bmc.txt) triggers the following error:

Unexpected Exception: java.lang.NullPointerException
Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: java.lang.NullPointerException
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:123)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:99)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:178)
Caused by: java.lang.NullPointerException
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:782)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:826)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1180)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:99)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:459)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2897)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1321)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:120)
        ... 3 more
jhoenicke commented 2 years ago

I fear that the check-sat-assuming command is broken again. As a work-around, you can assert the literals with assert and then use check-sat.

daniel-larraz commented 2 years ago

Simulating check-sat-assuming with a sequence of push, assert, check-sat, and pop gets around the problem. Thanks.