Check that predicate is not always false #26
Description
I can literally add #[ensures(false)] and the compiler doesn't even warn. Is there a way to provide a compilation warning if the predicate is detected to be always invalid?
{{ message }}
I can literally add #[ensures(false)] and the compiler doesn't even warn. Is there a way to provide a compilation warning if the predicate is detected to be always invalid?