Open samuelchassot opened 1 month ago
Be careful about semantics when using old
in nested functions, as this could lead to some ambuguity if there is variable shadowing: did the user mean old as "at the entry of the inner function", as in "at the entry of outer function". The behavior of whether the variable is considered changed by a nested function has changed recently in https://github.com/epfl-lara/stainless/pull/1532
It can be implemented a sugar instead of writing a
snapshot
at the beginning of the body:would be transformed into