Boulmé

Thanks. I got it (despite the fact that your answer may say `b` instead of `f``): observing a borrowed location before the end of its borrow is meaningless. Exactly, like...

I am not sure whether this is related, but I have difficulties to make FnMut closure work with reborrowing. For example, `foo_ok` is proved by Creusot/Alt-Ergo: ```rust fn foo_ok() {...

Thank you for your answer @jhjourdan, it clarifies a lot the picture for me. I know that there is no reason to create the borrow `c`, except that I wanted...

Here is the version with @jhjourdan specification: [main.rs.gz](https://github.com/xldenis/creusot/files/12736496/main.rs.gz) My log above gives the commit of Creusot. Is it enough for the bug report ? For the second issue: what are...