Better error message when pred not well funded.

nunchaku-inria / nunchaku

Model finder for higher-order logic

https://nunchaku-inria.github.io/nunchaku/

BSD 2-Clause "Simplified" License

42 stars 3 forks source link

Better error message when pred not well funded. #12

Closed ML44 closed 8 years ago

ML44 commented 8 years ago

Error message when pred not well funded.

File "src/transformations/Unroll.ml", line 111, characters 8-14: Assertion failed

Eg.

val u : type. val setminus : u -> u -> u. pred is_in : u -> u -> prop := forall a b x. ((is_in a x) && (~(is_in b x))) => (is_in (setminus a b) x). goal exists x a b. ~(is_in a x) && (is_in b x).