nokunish

Hi, I've also been having troubles with the type-invariant flags. If ``#[invariant(..)] `` is the only flag, Prusti doesn't seem to recognize it. ``` #[invariant(self.0 < 100)] pub struct ID(usize);...

It does not seem to make any difference... I've commented both/either one of them out, and they crash. I've also tried changing to `#[ensures(!result == self.is_none())]`,`#[ensures(result != self.is_none())]`, as well...

Hi, There seems to be a similar bug with `Option::Some(..)` as well. For instance, if we have a function that always returns `Some(usize)`, ``` #[pure] pub fn some_obj(&self) -> Option...

Hi, There might be a similar issue with mutually referential specifications. For instance, if we have ``` #[pure] #[trusted] #[ensures(result == nested_fn(_u))] pub fn is_true(_u: usize) -> bool { return...