-
Notifications
You must be signed in to change notification settings - Fork 19
(proof) Assertion error at FixResolutionProof.java:227 #115
Copy link
Copy link
Open
Description
Hi, for the following formula,
927.txt
smtinterpol
d208e93
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)
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels