smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

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

Open rainoftime opened this issue 4 years ago • 0 comments

Hi, for the following formula, 1904.txt

smtinterpol commit cb90e74

 Exception in thread "main" java.lang.AssertionError: Not an assumption in unsat clause
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkValidUnsatClause(DPLLEngine.java:1904)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getProof(DPLLEngine.java:1491)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.retrieveProof(SMTInterpol.java:1159)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getProof(SMTInterpol.java:791)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:883)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2933)
        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)

rainoftime avatar Jul 07 '20 07:07 rainoftime