search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
61 stars 17 forks source link

Assertion error at theory.cclosure.CCTerm.unshare(CCTerm.java:292) #122

Closed rainoftime closed 5 months ago

rainoftime commented 3 years ago

Hi, for the following formula, smtinterpol https://github.com/ultimate-pa/smtinterpol/commit/47ca37869cd94298f7e3fa3f0c642e854d73c24b 292.txt

sat
Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.unshare(CCTerm.java:292)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.pop(Clausifier.java:2047)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.pop(SMTInterpol.java:443)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2806)
        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)
jhoenicke commented 5 months ago

Cleaning up old issues. This seems to be fixed.