AssertionError at Interpolator.java:757 (incomplete fix)

[rainoftime]

Related: #74

---

Hi, for the following formula,
757.txt

smtinterpol commit f15aa21 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]

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.