AssertionError at theory.quant.QuantifierTheory.checkpoint(QuantifierTheory.java:191)

[rainoftime]

Hi, for the following formula

191.txt

smtinterpol (commit d768667) throws an assertion error

        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.checkpoint(QuantifierTheory.java:191)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateInternal(DPLLEngine.java:257)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1154)
        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.SMTInterpol.checkSat(SMTInterpol.java:429)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2896)
        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)

[tanjaschindler]

This should be solved by 5171d77