Dafny: fixed bug in which old locals were not properly forbidden from being modified during refinement

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index da0a733d..18f7cc61 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1603,7 +1603,9 @@ namespace Microsoft.Dafny {
       foreach (var lhs in stmt.Lhss) {

         var l = lhs.Resolved;

         if (l is IdentifierExpr) {

-          if (RefinementToken.IsInherited(l.tok, m) || ((IdentifierExpr)l).Var is Formal) {

+          var ident = (IdentifierExpr)l;

+          Contract.Assert(ident.Var is VarDecl || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)

+          if ((ident.Var is VarDecl && RefinementToken.IsInherited(((VarDecl)ident.Var).Tok, m)) || ident.Var is Formal) {

             // for some reason, formals are not considered to be inherited.

             reporter.Error(l.tok, "cannot assign to variable defined previously");

           }