search

ultimate-pa / smtinterpol

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

AssertionError at Clausifier.java:1120 #100

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula 1120.txt

smtinterpol commit db01df5 throws an assertion error

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLinVar(Clausifier.java:1120)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createAtom(EqualityProxy.java:158)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.getLiteral(EqualityProxy.java:186)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createCCEquality(EqualityProxy.java:109)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.createEquality(CClosure.java:1015)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.propagateSharedEquality(CCTerm.java:304)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.share(CCTerm.java:282)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.addSharedTerm(CClosure.java:784)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.share(Clausifier.java:1009)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.shareLATerm(Clausifier.java:1017)                                                                                     [8/1906]
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLinVar(Clausifier.java:1127)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createMutableAffinTerm(Clausifier.java:1137)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1082)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createAtom(EqualityProxy.java:140)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.getLiteral(EqualityProxy.java:186)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CollectLiteral.perform(Clausifier.java:588)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.run(Clausifier.java:1889)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addFormula(Clausifier.java:1957)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.assertTerm(SMTInterpol.java:650)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2881)
        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)
rainoftime commented 4 years ago

Merged to https://github.com/ultimate-pa/smtinterpol/issues/94