search

ultimate-pa / smtinterpol

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

AssertionError at FixResolutionProof.java:227 #102

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance, 227.txt

smtinterpol 7020e2605 throws an assertion error

 Exception in thread "main" java.lang.AssertionError: Unknown proof rule @assumption.
        at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.FixResolutionProof.walk(FixResolutionProof.java:227)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.FixResolutionProof$ProofWalker.walk(FixResolutionProof.java:70)
        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.proof.FixResolutionProof.fix(FixResolutionProof.java:189)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTermGenerator.convert(ProofTermGenerator.java:150)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getProof(SMTInterpol.java:782)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:537)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2916)
        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