Fix #1159 #1246
Fix #1159 #1246
Conversation
| case Old(v: Variable) if freshVarDecls.contains(v) => | ||
| Some(freshVars(freshVarDecls.indexOf(v))) |
There was a problem hiding this comment.
Ideally, this should be more restrictive and only apply within the postcondition to allow the ImperativeCleanup phase to correctly catch all incorrect uses of old. Could you maybe make this part of the extraVarReplace (e.g. by making it into a Map[Expr, Expr])?
There was a problem hiding this comment.
(I'll push an updated version)
There was a problem hiding this comment.
Actually, the Old(v) expression will already have its variable rewritten to its freshened variant (contained in freshVarDecls). I pushed a version that is simply passed a flag to tell us whether we should rewrite old expressions (less elegant, that's for sure...).
|
@samarion again it's marked "approved". Did you mean to just comment without clicking "approve"? |
Following the suggestion #1160 (comment)