Fixed bug introduced in changeset 7ebdf9cd4154

3 files changed, 17 insertions, 6 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 18b50686..7d3f570d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13760,9 +13760,9 @@ namespace Microsoft.Dafny {
           }

 

           var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension);

-          Expression newRange = e.Range == null ? null : Substitute(e.Range);

-          Expression newTerm = Substitute(e.Term);

-          Attributes newAttrs = SubstAttributes(e.Attributes);

+          var newRange = e.Range == null ? null : Substitute(e.Range);

+          var newTerm = Substitute(e.Term);

+          var newAttrs = SubstAttributes(e.Attributes);

           if (newBoundVars != e.BoundVars || newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

             if (e is SetComprehension) {

               newExpr = new SetComprehension(expr.tok, ((SetComprehension)e).Finite, newBoundVars, newRange, newTerm, newAttrs);

@@ -13778,9 +13778,9 @@ namespace Microsoft.Dafny {
             } else {

               Contract.Assert(false);  // unexpected ComprehensionExpr

             }

-          }

-          if (e.Bounds != null) {

-            ((ComprehensionExpr)newExpr).Bounds = e.Bounds.ConvertAll(bound => SubstituteBoundedPool(bound));

+            if (e.Bounds != null) {

+              ((ComprehensionExpr)newExpr).Bounds = e.Bounds.ConvertAll(bound => SubstituteBoundedPool(bound));

+            }

           }

           // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)

           foreach (var bv in e.BoundVars) {

diff --git a/Test/dafny4/Regression1.dfy b/Test/dafny4/Regression1.dfy
new file mode 100644
index 00000000..ebd8cf6d
--- /dev/null
+++ b/Test/dafny4/Regression1.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+ghost method M() {

+  var x :=

+// In the following line, why are the range and term copied in Substitute?

+//    var loo := 100; map y | 0 <= y < 100 :: y+1;

+    var loo := 100; imap y: int | true :: 3;

+}

diff --git a/Test/dafny4/Regression1.dfy.expect b/Test/dafny4/Regression1.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny4/Regression1.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors