Fix issue #63. ForceSubstitutionOfQuantifiedVars for SetComprehesion.

3 files changed, 17 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a150eecd..f3572948 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -13418,9 +13418,9 @@ namespace Microsoft.Dafny {
           newExpr = new NamedExpr(e.tok, e.Name, body, contract, e.ReplacerToken);

         } else if (expr is ComprehensionExpr) {

           var e = (ComprehensionExpr)expr;

-          // For quantifiers we want to make sure that we don't introduce name clashes with

+          // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with

           // the enclosing scopes.

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

+          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);

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

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

+

+method M()

+  modifies set o: object | true

+{

+}

+

+method Client()

+{

+  assume forall o: object :: o != null ==> false;

+  M();

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug63.dfy.expect b/Test/dafny4/Bug63.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny4/Bug63.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors