smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

(proof) Assertion error at FixResolutionProof.java:227

Open rainoftime opened this issue 4 years ago • 0 comments

Hi, for the following formula, 927.txt

smtinterpol d208e931d9

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:799)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2949)

rainoftime avatar Sep 24 '20 05:09 rainoftime