AssertionError at theory.cclosure.CClosure.removeCompareTrigger(CClosure.java:505)

[rainoftime]

Hi, for the following formula
505.txt

smtinterpol 5171d77 throws an assetion error:

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.removeCompareTrigger(CClosure.java:505)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.ematching.EMatching$EMUndoInformation.undo(EMatching.java:485)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.ematching.EMatching.undo(EMatching.java:200)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.ematching.EMatching.removeAllTriggers(EMatching.java:149)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.quant.QuantifierTheory.pop(QuantifierTheory.java:350)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.pop(DPLLEngine.java:1458)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.pop(Clausifier.java:1980)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.pop(SMTInterpol.java:424)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2836)
        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)

[jhoenicke]

Should be fixed by 5171d77

[tanjaschindler]

I still get the assertion error.

[tanjaschindler]

Thanks for the report! This should be fixed by 0610d35 .