Aurea

@kevinresol Yes, I added that after your first comment. If a library function returns a native enum, it's fine in C, where it is just an integer. So the method...

Yeah, that looks almost like an ADT. At the moment that is not mappable to an enum for sure (without writing your own mapping). I'll have to think about this...

I have run into cases where the warning was emitted, even though nothing actually went wrong. It should not be a compilation error unless it is made more reliable.

Thanks for the report. The feature you are looking for, type invariants, is something we used to support in Prusti. The syntax would be `#[invariant(...)]` attached to the `struct`. However,...

> Which is a _different_ `unreachable!()` than the one @fpoli pointed to. It is a different line, but unfortunately the `unreachable!()` is reached for the same reason, which is the...

Looks good. Although we indeed might not want to explain snapshots fully (we've had this discussion a couple of times already!), we could at least note that snapshots follow nested...

Thanks! ~~The stderr tee looks a bit hacky, I think it would have been fine to keep the error message from `cargo` and explain what it means in one of...

> 1. Instead of a sequence of inhales, the impure encoding could inhale just a single quantification. This seems an easy fix. > ``` > forall i: Int :: 0...

Does it work if you spell out the `old`, i.e. `#[ensures(old(&out).inner === old(&out).inner)]` (or any variant thereof)? The `===` is syntax sugar for `snapshot_equality(&out.inner, &out.inner)` here, does a similar error...

This is a duplicate of #797 then, I think.