search

cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Check side condition return type #15

Closed ajreynol closed 5 years ago

ajreynol commented 5 years ago

This ensures we check that the return type of side conditions matches the body of the side condition.

Unfortunately I don't think there a test I can add to exercise this fix (since this would require infrastructure for testing failing LFSC tests).

ajreynol commented 5 years ago

For reference, here is a file that would previously pass when it should not:

(declare bool type)
(declare tt bool)
(declare ff bool)

(program f1 ((n mpz)) mpz
  (mp_ifneg n tt ff)
)