smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

AssertionError at DPLLEngine.java:704 (check-allsat)

Open rainoftime opened this issue 4 years ago • 0 comments

Hi, for the following formula, 704.txt

smtinterpol commit cb90e74

sat
 Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:704)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:854)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.access$100(DPLLEngine.java:56)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine$AllSatIterator.hasNext(DPLLEngine.java:1791)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.convertSexp(SExpression.java:58)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.toString(SExpression.java:82)
        at java.lang.String.valueOf(String.java:2994)
        at java.io.PrintWriter.println(PrintWriter.java:754)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.printResponse(ParseEnvironment.java:168)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:3154)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1317)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:119)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:98)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:165)

rainoftime avatar Jul 07 '20 06:07 rainoftime