search

ultimate-pa / smtinterpol

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

AssertionError at Interpolator.java:757 (incomplete fix) #96

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Related: https://github.com/ultimate-pa/smtinterpol/issues/74

Hi, for the following formula, 757.txt

smtinterpol commit f15aa2170 throws an assertion error

unsat
 Exception in thread "main" java.lang.AssertionError: Mixed Literal with only one subterm: r1 + -9409/1000000 atom: (! (<= (+ r1 (/ (- 9409.0) 1000000.0)) 0.0) :quotedLA)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.colorMixedLiteral(Interpolator.java:757)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getAtomOccurenceInfo(Interpolator.java:707)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.LAInterpolator.computeInterpolants(LAInterpolator.java:174)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.walkLeafNode(Interpolator.java:303)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.access$100(Interpolator.java:61)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator$ProofTreeWalker.walk(Interpolator.java:138)
        at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:115)
        at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:106)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:239)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:216)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:866)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2953)
        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 commented 4 years ago

Note to self: the problem here is that r1 occurs in the proof only in quantifier inputs, which are not yet supported. This probably solves itself, when we rework proof production for quantified clauses.

There is another potential issue here, though. If a symbol occurs in the proof, but in no input formula (unlikely, but nothing prevents the proof to contain unnecessary steps involving symbols that are not needed), then the same problem would occur. We may need to put such symbols into some dummy partition.