search

cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Guard when markvar or ifmarked are applied to a non-variable #72

Closed ajreynol closed 2 years ago

ajreynol commented 2 years ago

Fixes https://github.com/cvc5/LFSC/issues/71

BrunoDutertre commented 2 years ago

The same bug is in the ifmarked case. Line 618:

      if (!tptp->isType(statType))