Fix issue #63. ForceSubstitutionOfQuantifiedVars for SetComprehesion.

1 files changed, 2 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);