Samuel Chassot
Samuel Chassot
It can be implemented a sugar instead of writing a `snapshot` at the beginning of the body: ``` def f() = // mutable operations assert(old(this).size > this.size) // ... ```...
Idea: provision the timeout for more than 1 unrolling to avoid spending the entire timeout in the first unrolling step. This would (maybe) allow the automatic verification of properties that...