smtinterpol
smtinterpol copied to clipboard
(proof) Assertion error at FixResolutionProof.java:227
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)