From cb760d823372f0d6a45469cb7840cad9df023232 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Thu, 22 Oct 2015 21:46:42 -0700
Subject: Fixed bug introduced in changeset 7ebdf9cd4154

---
 Source/Dafny/Translator.cs         | 12 ++++++------
 Test/dafny4/Regression1.dfy        |  9 +++++++++
 Test/dafny4/Regression1.dfy.expect |  2 ++
 3 files changed, 17 insertions(+), 6 deletions(-)
 create mode 100644 Test/dafny4/Regression1.dfy
 create mode 100644 Test/dafny4/Regression1.dfy.expect

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
-- 
cgit v1.2.3