smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

AssertionError at DPLLEngine.java:1514 (incomplete fix)

Open rainoftime opened this issue 4 years ago • 0 comments

Related and fixed https://github.com/ultimate-pa/smtinterpol/issues/76


Hi, for the following formulas, xx.txt 1514.txt

SMTInterpol (commit 7625fe26c8f2) throws an AssertionError

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.generateLevel0Proof(DPLLEngine.java:1514)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.setLiteral(DPLLEngine.java:457)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateClauses(DPLLEngine.java:402)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateInternal(DPLLEngine.java:243)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1148)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2916)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1311)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:133)
        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)

rainoftime avatar Apr 25 '20 15:04 rainoftime