Refactor resolver, and really allow reads to take fields of type A -> set<obj>

twoState and codeContext is moved to a new class ResolveOpts

5 files changed, 248 insertions, 176 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 61b5ccff..60f40784 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -563,7 +563,7 @@ namespace Microsoft.Dafny
       var datatypeDependencies = new Graph<IndDatatypeDecl>();

       var codatatypeDependencies = new Graph<CoDatatypeDecl>();

       int prevErrorCount = ErrorCount;

-      ResolveAttributes(m.Attributes, false, new NoContext(m.Module));

+      ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false));

       ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

       if (ErrorCount == prevErrorCount) {

         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

@@ -1522,7 +1522,7 @@ namespace Microsoft.Dafny
         ResolveTypeParameters(d.TypeArgs, false, d);

         if (!(d is IteratorDecl)) {

           // Note, attributes of iterators are resolved by ResolvedIterator, after registering any names in the iterator signature

-          ResolveAttributes(d.Attributes, false, new NoContext(d.Module));

+          ResolveAttributes(d.Attributes, new ResolveOpts(new NoContext(d.Module), false));

         }

         if (d is IteratorDecl) {

           var iter = (IteratorDecl)d;

@@ -3034,7 +3034,7 @@ namespace Microsoft.Dafny
       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         if (member is Field) {

-          ResolveAttributes(member.Attributes, false, new NoContext(currentClass.Module));

+          ResolveAttributes(member.Attributes, new ResolveOpts(new NoContext(currentClass.Module), false));

           // nothing more to do

 

         } else if (member is Function) {

@@ -3319,21 +3319,21 @@ namespace Microsoft.Dafny
       }

     }

 

-    void ResolveAttributes(Attributes attrs, bool twoState, ICodeContext codeContext) {

+    void ResolveAttributes(Attributes attrs, ResolveOpts opts) {

       // order does not matter much for resolution, so resolve them in reverse order

       for (; attrs != null; attrs = attrs.Prev) {

         if (attrs.Args != null) {

-          ResolveAttributeArgs(attrs.Args, twoState, codeContext, true);

+          ResolveAttributeArgs(attrs.Args, opts, true);

         }

       }

     }

 

-    void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState, ICodeContext codeContext, bool allowGhosts) {

+    void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, ResolveOpts opts, bool allowGhosts) {

       Contract.Requires(args != null);

       foreach (Attributes.Argument aa in args) {

         Contract.Assert(aa != null);

         if (aa.E != null) {

-          ResolveExpression(aa.E, twoState, codeContext);

+          ResolveExpression(aa.E, opts);

           if (!allowGhosts) {

             CheckIsNonGhost(aa.E);

           }

@@ -3390,9 +3390,9 @@ namespace Microsoft.Dafny
       foreach (Formal p in f.Formals) {

         scope.Push(p.Name, p);

       }

-      ResolveAttributes(f.Attributes, false, f);

+      ResolveAttributes(f.Attributes, new ResolveOpts(f, false));

       foreach (Expression r in f.Req) {

-        ResolveExpression(r, false, f);

+        ResolveExpression(r, new ResolveOpts(f, false));

         Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(r.Type, Type.Bool)) {

           Error(r, "Precondition must be a boolean (got {0})", r.Type);

@@ -3402,20 +3402,20 @@ namespace Microsoft.Dafny
         ResolveFrameExpression(fr, "reads", f.IsGhost, f);

       }

       foreach (Expression r in f.Ens) {

-        ResolveExpression(r, false, f);  // since this is a function, the postcondition is still a one-state predicate

+        ResolveExpression(r, new ResolveOpts(f, false));  // since this is a function, the postcondition is still a one-state predicate

         Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(r.Type, Type.Bool)) {

           Error(r, "Postcondition must be a boolean (got {0})", r.Type);

         }

       }

-      ResolveAttributes(f.Decreases.Attributes, false, f);

+      ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false));

       foreach (Expression r in f.Decreases.Expressions) {

-        ResolveExpression(r, false, f);

+        ResolveExpression(r, new ResolveOpts(f, false));

         // any type is fine

       }

       if (f.Body != null) {

         var prevErrorCount = ErrorCount;

-        ResolveExpression(f.Body, false, f);

+        ResolveExpression(f.Body, new ResolveOpts(f, false));

         if (!f.IsGhost && prevErrorCount == ErrorCount) {

           CheckIsNonGhost(f.Body);

         }

@@ -3431,9 +3431,13 @@ namespace Microsoft.Dafny
       Contract.Requires(fe != null);

       Contract.Requires(kind != null);

       Contract.Requires(codeContext != null);

-      ResolveExpression(fe.E, false, codeContext);

+      ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));

       Type t = fe.E.Type;

       Contract.Assert(t != null);  // follows from postcondition of ResolveExpression

+      var arrTy = t.NormalizeExpand() as ArrowType;

+      if (arrTy != null) {

+        t = arrTy.Result;

+      }

       var collType = t.AsCollectionType;

       if (collType != null) {

         t = collType.Arg;

@@ -3505,14 +3509,14 @@ namespace Microsoft.Dafny
 

         // Start resolving specification...

         foreach (MaybeFreeExpression e in m.Req) {

-          ResolveAttributes(e.Attributes, false, m);

-          ResolveExpression(e.E, false, m);

+          ResolveAttributes(e.Attributes, new ResolveOpts(m, false));

+          ResolveExpression(e.E, new ResolveOpts(m, false));

           Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.E.Type, Type.Bool)) {

             Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

           }

         }

-        ResolveAttributes(m.Mod.Attributes, false, m);

+        ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false));

         foreach (FrameExpression fe in m.Mod.Expressions) {

           ResolveFrameExpression(fe, "modifies", m.IsGhost, m);

           if (m is Lemma) {

@@ -3521,9 +3525,9 @@ namespace Microsoft.Dafny
             Error(fe.tok, "colemmas are not allowed to have modifies clauses");

           }

         }

-        ResolveAttributes(m.Decreases.Attributes, false, m);

+        ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false));

         foreach (Expression e in m.Decreases.Expressions) {

-          ResolveExpression(e, false, m);

+          ResolveExpression(e, new ResolveOpts(m, false));

           // any type is fine

           if (m.IsGhost && e is WildcardExpr) {

             Error(e, "'decreases *' is not allowed on ghost methods");

@@ -3543,8 +3547,8 @@ namespace Microsoft.Dafny
 

         // ... continue resolving specification

         foreach (MaybeFreeExpression e in m.Ens) {

-          ResolveAttributes(e.Attributes, true, m);

-          ResolveExpression(e.E, true, m);

+          ResolveAttributes(e.Attributes, new ResolveOpts(m, true));

+          ResolveExpression(e.E, new ResolveOpts(m, true));

           Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.E.Type, Type.Bool)) {

             Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

@@ -3565,7 +3569,7 @@ namespace Microsoft.Dafny
         }

 

         // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)

-        ResolveAttributes(m.Attributes, false, m);

+        ResolveAttributes(m.Attributes, new ResolveOpts(m, false));

 

         scope.PopMarker();  // for the out-parameters and outermost-level locals

         scope.PopMarker();  // for the in-parameters

@@ -3628,7 +3632,7 @@ namespace Microsoft.Dafny
       Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);

       for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {

         var e = iter.Decreases.Expressions[i];

-        ResolveExpression(e, false, iter);

+        ResolveExpression(e, new ResolveOpts(iter, false));

         // any type is fine, but associate this type with the corresponding _decreases<n> field

         var d = iter.DecreasesFields[i];

         if (!UnifyTypes(d.Type, e.Type)) {

@@ -3643,7 +3647,7 @@ namespace Microsoft.Dafny
         ResolveFrameExpression(fe, "modifies", false, iter);

       }

       foreach (MaybeFreeExpression e in iter.Requires) {

-        ResolveExpression(e.E, false, iter);

+        ResolveExpression(e.E, new ResolveOpts(iter, false));

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);

@@ -3659,28 +3663,28 @@ namespace Microsoft.Dafny
       Contract.Assert(scope.AllowInstance);

 

       foreach (MaybeFreeExpression e in iter.YieldRequires) {

-        ResolveExpression(e.E, false, iter);

+        ResolveExpression(e.E, new ResolveOpts(iter, false));

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);

         }

       }

       foreach (MaybeFreeExpression e in iter.YieldEnsures) {

-        ResolveExpression(e.E, true, iter);

+        ResolveExpression(e.E, new ResolveOpts(iter, true));

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

       foreach (MaybeFreeExpression e in iter.Ensures) {

-        ResolveExpression(e.E, true, iter);

+        ResolveExpression(e.E, new ResolveOpts(iter, true));

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E.Type, Type.Bool)) {

           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

 

-      ResolveAttributes(iter.Attributes, false, iter);

+      ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false));

 

       var postSpecErrorCount = ErrorCount;

 

@@ -4445,12 +4449,12 @@ namespace Microsoft.Dafny
     public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {

       Contract.Requires(stmt != null);

       Contract.Requires(codeContext != null);

-      ResolveAttributes(stmt.Attributes, true, codeContext);

+      ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true));

       if (stmt is PredicateStmt) {

         PredicateStmt s = (PredicateStmt)stmt;

-        ResolveAttributes(s.Attributes, false, codeContext);

+        ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, false));

         s.IsGhost = true;

-        ResolveExpression(s.Expr, true, codeContext);

+        ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));

         Contract.Assert(s.Expr.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(s.Expr.Type, Type.Bool)) {

           Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);

@@ -4458,7 +4462,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

-        ResolveAttributeArgs(s.Args, false, codeContext, false);

+        ResolveAttributeArgs(s.Args, new ResolveOpts(codeContext, false), false);

         if (specContextOnly) {

           Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

         }

@@ -4524,7 +4528,7 @@ namespace Microsoft.Dafny
                 produceLhs = ident;

               } else {

                 var yieldIdent = new MemberSelectExpr(f.tok, new ImplicitThisExpr(f.tok), f.Name);

-                ResolveExpression(yieldIdent, true, codeContext);

+                ResolveExpression(yieldIdent, new ResolveOpts(codeContext, true));

                 produceLhs = yieldIdent;

               }

               formals.Add(produceLhs);

@@ -4635,7 +4639,7 @@ namespace Microsoft.Dafny
       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         int prevErrorCount = ErrorCount;

-        ResolveExpression(s.Lhs, true, codeContext);  // allow ghosts for now, tighted up below

+        ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true));  // allow ghosts for now, tighted up below

         bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;

         Contract.Assert(s.Lhs.Type != null);  // follows from postcondition of ResolveExpression

         // check that LHS denotes a mutable variable or a field

@@ -4714,7 +4718,7 @@ namespace Microsoft.Dafny
         Type lhsType = s.Lhs.Type;

         if (s.Rhs is ExprRhs) {

           ExprRhs rr = (ExprRhs)s.Rhs;

-          ResolveExpression(rr.Expr, true, codeContext);

+          ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true));

           if (!lvalueIsGhost) {

             CheckIsNonGhost(rr.Expr);

           }

@@ -4764,7 +4768,7 @@ namespace Microsoft.Dafny
         bool branchesAreSpecOnly = specContextOnly;

         if (s.Guard != null) {

           int prevErrorCount = ErrorCount;

-          ResolveExpression(s.Guard, true, codeContext);

+          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));

           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression

           bool successfullyResolved = ErrorCount == prevErrorCount;

           if (!UnifyTypes(s.Guard.Type, Type.Bool)) {

@@ -4796,7 +4800,7 @@ namespace Microsoft.Dafny
         bool bodyMustBeSpecOnly = specContextOnly;

         if (s.Guard != null) {

           int prevErrorCount = ErrorCount;

-          ResolveExpression(s.Guard, true, codeContext);

+          ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));

           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression

           bool successfullyResolved = ErrorCount == prevErrorCount;

           if (!UnifyTypes(s.Guard.Type, Type.Bool)) {

@@ -4808,17 +4812,17 @@ namespace Microsoft.Dafny
         }

 

         foreach (MaybeFreeExpression inv in s.Invariants) {

-          ResolveAttributes(inv.Attributes, true, codeContext);

-          ResolveExpression(inv.E, true, codeContext);

+          ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true));

+          ResolveExpression(inv.E, new ResolveOpts(codeContext, true));

           Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(inv.E.Type, Type.Bool)) {

             Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);

           }

         }

 

-        ResolveAttributes(s.Decreases.Attributes, true, codeContext);

+        ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true));

         foreach (Expression e in s.Decreases.Expressions) {

-          ResolveExpression(e, true, codeContext);

+          ResolveExpression(e, new ResolveOpts(codeContext, true));

           if (bodyMustBeSpecOnly && e is WildcardExpr) {

             Error(e, "'decreases *' is not allowed on ghost loops");

           }

@@ -4826,7 +4830,7 @@ namespace Microsoft.Dafny
         }

 

         if (s.Mod.Expressions != null) {

-          ResolveAttributes(s.Mod.Attributes, true, codeContext);

+          ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));

           foreach (FrameExpression fe in s.Mod.Expressions) {

             ResolveFrameExpression(fe, "modifies", bodyMustBeSpecOnly, codeContext);

           }

@@ -4844,7 +4848,7 @@ namespace Microsoft.Dafny
         var s = (AlternativeLoopStmt)stmt;

         s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);

         foreach (MaybeFreeExpression inv in s.Invariants) {

-          ResolveExpression(inv.E, true, codeContext);

+          ResolveExpression(inv.E, new ResolveOpts(codeContext, true));

           Contract.Assert(inv.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(inv.E.Type, Type.Bool)) {

             Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);

@@ -4852,7 +4856,7 @@ namespace Microsoft.Dafny
         }

 

         foreach (Expression e in s.Decreases.Expressions) {

-          ResolveExpression(e, true, codeContext);

+          ResolveExpression(e, new ResolveOpts(codeContext, true));

           if (s.IsGhost && e is WildcardExpr) {

             Error(e, "'decreases *' is not allowed on ghost loops");

           }

@@ -4870,13 +4874,13 @@ namespace Microsoft.Dafny
           }

           ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

-        ResolveExpression(s.Range, true, codeContext);

+        ResolveExpression(s.Range, new ResolveOpts(codeContext, true));

         Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(s.Range.Type, Type.Bool)) {

           Error(stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);

         }

         foreach (var ens in s.Ens) {

-          ResolveExpression(ens.E, true, codeContext);

+          ResolveExpression(ens.E, new ResolveOpts(codeContext, true));

           Contract.Assert(ens.E.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(ens.E.Type, Type.Bool)) {

             Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);

@@ -4884,7 +4888,7 @@ namespace Microsoft.Dafny
         }

         // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them

         // first (above) and only then resolve the attributes (below).

-        ResolveAttributes(s.Attributes, true, codeContext);

+        ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));

 

         bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));

         if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {

@@ -4950,7 +4954,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is ModifyStmt) {

         var s = (ModifyStmt)stmt;

-        ResolveAttributes(s.Mod.Attributes, true, codeContext);

+        ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));

         foreach (FrameExpression fe in s.Mod.Expressions) {

           // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message

           ResolveFrameExpression(fe, "modifies", specContextOnly, codeContext);

@@ -4966,18 +4970,18 @@ namespace Microsoft.Dafny
         s.IsGhost = true;

         if (s.Lines.Count > 0) {

           var e0 = s.Lines.First();

-          ResolveExpression(e0, true, codeContext);

+          ResolveExpression(e0, new ResolveOpts(codeContext, true));

           Contract.Assert(e0.Type != null);  // follows from postcondition of ResolveExpression

           for (int i = 1; i < s.Lines.Count; i++) {

             if (i < s.Lines.Count - 1 || prevErrorCount == ErrorCount) { // do not resolve the dummy step if there were errors, it might generate more errors

               var e1 = s.Lines[i];

-              ResolveExpression(e1, true, codeContext);

+              ResolveExpression(e1, new ResolveOpts(codeContext, true));

               Contract.Assert(e1.Type != null);  // follows from postcondition of ResolveExpression

               if (!UnifyTypes(e0.Type, e1.Type)) {

                 Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);

               } else {

                 var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator

-                ResolveExpression(step, true, codeContext);

+                ResolveExpression(step, new ResolveOpts(codeContext, true));

                 s.Steps.Add(step);

               }

               e0 = e1;

@@ -5003,7 +5007,7 @@ namespace Microsoft.Dafny
         } else {

           s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0));

         }

-        ResolveExpression(s.Result, true, codeContext);

+        ResolveExpression(s.Result, new ResolveOpts(codeContext, true));

         Contract.Assert(s.Result != null);

         Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);

 

@@ -5011,7 +5015,7 @@ namespace Microsoft.Dafny
         MatchStmt s = (MatchStmt)stmt;

         bool bodyIsSpecOnly = specContextOnly;

         int prevErrorCount = ErrorCount;

-        ResolveExpression(s.Source, true, codeContext);

+        ResolveExpression(s.Source, new ResolveOpts(codeContext, true));

         Contract.Assert(s.Source.Type != null);  // follows from postcondition of ResolveExpression

         bool successfullyResolved = ErrorCount == prevErrorCount;

         if (!specContextOnly && successfullyResolved) {

@@ -5191,7 +5195,7 @@ namespace Microsoft.Dafny
       var lhsNameSet = new HashSet<string>();  // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)

       foreach (var lhs in s.Lhss) {

         var ec = ErrorCount;

-        ResolveExpression(lhs, true, codeContext);

+        ResolveExpression(lhs, new ResolveOpts(codeContext, true));

         if (ec == ErrorCount) {

           if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs) && !codeContext.IsGhost) {

             Error(lhs, "cannot assign to non-ghost variable in a ghost context");

@@ -5243,15 +5247,15 @@ namespace Microsoft.Dafny
         } else {

           var er = (ExprRhs)rhs;

           if (er.Expr is IdentifierSequence) {

-            var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, codeContext, true);

+            var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, new ResolveOpts(codeContext, true), true);

             isEffectful = cRhs != null;

             callRhs = callRhs ?? cRhs;

           } else if (er.Expr is FunctionCallExpr) {

-            var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, codeContext, true);

+            var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, new ResolveOpts(codeContext, true), true);

             isEffectful = cRhs != null;

             callRhs = callRhs ?? cRhs;

           } else {

-            ResolveExpression(er.Expr, true, codeContext);

+            ResolveExpression(er.Expr, new ResolveOpts(codeContext, true));

             isEffectful = false;

           }

         }

@@ -5345,7 +5349,7 @@ namespace Microsoft.Dafny
 

       s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);

       var ec = ErrorCount;

-      ResolveExpression(s.Expr, true, codeContext);

+      ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));

       if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {

         CheckIsNonGhost(s.Expr);

 

@@ -5374,7 +5378,7 @@ namespace Microsoft.Dafny
       // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement

       foreach (var alternative in alternatives) {

         int prevErrorCount = ErrorCount;

-        ResolveExpression(alternative.Guard, true, codeContext);

+        ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));

         Contract.Assert(alternative.Guard.Type != null);  // follows from postcondition of ResolveExpression

         bool successfullyResolved = ErrorCount == prevErrorCount;

         if (!UnifyTypes(alternative.Guard.Type, Type.Bool)) {

@@ -5415,7 +5419,7 @@ namespace Microsoft.Dafny
       bool isInitCall = receiverType != null;

 

       // resolve receiver

-      ResolveReceiver(s.Receiver, true, codeContext);

+      ResolveReceiver(s.Receiver, new ResolveOpts(codeContext, true));

       Contract.Assert(s.Receiver.Type != null);  // follows from postcondition of ResolveExpression

       if (receiverType == null) {

         receiverType = s.Receiver.Type;

@@ -5452,7 +5456,7 @@ namespace Microsoft.Dafny
       foreach (Expression e in s.Args) {

         bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;

         var ec = ErrorCount;

-        ResolveExpression(e, true, codeContext);

+        ResolveExpression(e, new ResolveOpts(codeContext, true));

         if (ec == ErrorCount && !allowGhost) {

           CheckIsNonGhost(e);

         }

@@ -5898,7 +5902,7 @@ namespace Microsoft.Dafny
           int i = 0;

           foreach (Expression dim in rr.ArrayDimensions) {

             Contract.Assert(dim != null);

-            ResolveExpression(dim, true, codeContext);

+            ResolveExpression(dim, new ResolveOpts(codeContext, true));

             if (!UnifyTypes(dim.Type, Type.Int)) {

               Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);

             }

@@ -6164,12 +6168,34 @@ namespace Microsoft.Dafny
       return GetThisType(tok, (ClassDecl)member.EnclosingClass);

     }

 

+    public class ResolveOpts

+    {

+      public readonly ICodeContext codeContext;

+      public readonly bool twoState;

+      public readonly bool IsGhost;

+      public ResolveOpts(ICodeContext codeContext, bool twoState) {

+        this.codeContext = codeContext;

+        this.twoState = twoState;

+        IsGhost = codeContext.IsGhost;

+      }

+      public ResolveOpts(ICodeContext codeContext, bool twoState, bool isGhost) {

+        this.codeContext = codeContext;

+        this.twoState = twoState;

+        this.IsGhost = isGhost;

+      }

+      public ResolveOpts(ResolveOpts r, bool isGhost) {

+        codeContext = r.codeContext;

+        twoState = r.twoState;

+        this.IsGhost = isGhost;

+      }

+    }

+

     /// <summary>

     /// "twoState" implies that "old" and "fresh" expressions are allowed.

     /// </summary>

-    public void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) {

+    public void ResolveExpression(Expression expr, ResolveOpts opts) {

 #if TEST_TYPE_SYNONYM_TRANSPARENCY

-      ResolveExpressionX(expr, twoState, codeContext);

+      ResolveExpressionX(expr, opts);

       // For testing purposes, change the type of "expr" to a type synonym (mwo-ha-ha-ha!)

       var t = expr.Type;

       Contract.Assert(t != null);

@@ -6177,10 +6203,10 @@ namespace Microsoft.Dafny
       var ts = new UserDefinedType(expr.tok, "type#synonym#transparency#test", sd, new List<Type>(), null);

       expr.DebugTest_ChangeType(ts);

     }

-    public void ResolveExpressionX(Expression expr, bool twoState, ICodeContext codeContext) {

+    public void ResolveExpressionX(Expression expr, ResolveOpts opts) {

 #endif

       Contract.Requires(expr != null);

-      Contract.Requires(codeContext != null);

+      Contract.Requires(opts != null);

       Contract.Ensures(expr.Type != null);

       if (expr.Type != null) {

         // expression has already been resovled

@@ -6194,24 +6220,24 @@ namespace Microsoft.Dafny
 

       if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         e.ResolvedExpression = e.E;

         e.Type = e.E.Type;

 

       } else if (expr is ChainingExpression) {

         var e = (ChainingExpression)expr;

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         e.ResolvedExpression = e.E;

         e.Type = e.E.Type;

 

       } else if (expr is IdentifierSequence) {

         var e = (IdentifierSequence)expr;

-        ResolveIdentifierSequence(e, twoState, codeContext, false);

+        ResolveIdentifierSequence(e, opts, false);

 

       } else if (expr is NegationExpression) {

         var e = (NegationExpression)expr;

         var errorCount = ErrorCount;

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         e.Type = e.E.Type;

         if (errorCount != ErrorCount) {

           // there were errors resolving the operand; take the quick way out and

@@ -6232,7 +6258,7 @@ namespace Microsoft.Dafny
           // Resolve the subtraction expression.  This look like it will resolve e.E once more,

           // but the recursive calls to the resolver is mindful about DAGs and will check if the

           // subexpression has already been resolved.

-          ResolveExpression(subtract, twoState, codeContext);

+          ResolveExpression(subtract, opts);

           e.ResolvedExpression = subtract;

         }

 

@@ -6283,14 +6309,14 @@ namespace Microsoft.Dafny
         } else if (!(d is DatatypeDecl)) {

           Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);

         } else {

-          ResolveDatatypeValue(twoState, codeContext, dtv, (DatatypeDecl)d);

+          ResolveDatatypeValue(opts, dtv, (DatatypeDecl)d);

         }

 

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         Type elementType = new InferredTypeProxy();

         foreach (Expression ee in e.Elements) {

-          ResolveExpression(ee, twoState, codeContext);

+          ResolveExpression(ee, opts);

           Contract.Assert(ee.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(elementType, ee.Type)) {

             Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);

@@ -6308,12 +6334,12 @@ namespace Microsoft.Dafny
         Type domainType = new InferredTypeProxy();

         Type rangeType = new InferredTypeProxy();

         foreach (ExpressionPair p in e.Elements) {

-          ResolveExpression(p.A, twoState, codeContext);

+          ResolveExpression(p.A, opts);

           Contract.Assert(p.A.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(domainType, p.A.Type)) {

             Error(p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);

           }

-          ResolveExpression(p.B, twoState, codeContext);

+          ResolveExpression(p.B, opts);

           Contract.Assert(p.B.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(rangeType, p.B.Type)) {

             Error(p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);

@@ -6326,7 +6352,7 @@ namespace Microsoft.Dafny
         // The following call to ResolveExpression is just preliminary.  If it succeeds, it is redone below on the resolved expression.  Thus,

         // it's okay to be more lenient here and use coLevel (instead of trying to use CoLevel_Dec(coLevel), which is needed when .Name denotes a

         // destructor for a co-datatype).

-        ResolveExpression(e.Obj, twoState, codeContext);

+        ResolveExpression(e.Obj, opts);

         Contract.Assert(e.Obj.Type != null);  // follows from postcondition of ResolveExpression

         Expression resolved = ResolveMemberSelect(expr.tok, e.Obj, e.SuffixName);

 

@@ -6335,13 +6361,13 @@ namespace Microsoft.Dafny
         } else {

           // the following will cause e.Obj to be resolved again, but that's still correct 

           e.ResolvedExpression = resolved;

-          ResolveExpression(e.ResolvedExpression, twoState, codeContext);

+          ResolveExpression(e.ResolvedExpression, opts);

           e.Type = e.ResolvedExpression.Type;

         }

 

       } else if (expr is MemberSelectExpr) {

         var e = (MemberSelectExpr)expr;

-        ResolveExpression(e.Obj, twoState, codeContext);

+        ResolveExpression(e.Obj, opts);

         Contract.Assert(e.Obj.Type != null);  // follows from postcondition of ResolveExpression

         NonProxyType nptype;

         MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.MemberName, out nptype);

@@ -6363,7 +6389,7 @@ namespace Microsoft.Dafny
             e.TypeApplication.Add(prox);

           }

           e.Type = SubstType(fn.Type, subst);

-          AddCallGraphEdge(e, codeContext, fn);

+          AddCallGraphEdge(e, opts.codeContext, fn);

         } else if (!(member is Field)) {

           Error(expr, "member {0} in type {1} does not refer to a field or a function", e.MemberName,

             cce.NonNull(ctype).Name);

@@ -6382,12 +6408,12 @@ namespace Microsoft.Dafny
 

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

-        ResolveSeqSelectExpr(e, twoState, codeContext, true);

+        ResolveSeqSelectExpr(e, opts, true);

 

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

 

-        ResolveExpression(e.Array, twoState, codeContext);

+        ResolveExpression(e.Array, opts);

         Contract.Assert(e.Array.Type != null);  // follows from postcondition of ResolveExpression

         Type elementType = new InferredTypeProxy();

         if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType))) {

@@ -6396,7 +6422,7 @@ namespace Microsoft.Dafny
         int i = 0;

         foreach (Expression idx in e.Indices) {

           Contract.Assert(idx != null);

-          ResolveExpression(idx, twoState, codeContext);

+          ResolveExpression(idx, opts);

           Contract.Assert(idx.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(idx.Type, Type.Int)) {

             Error(idx, "array selection requires integer indices (got {0} for index {1})", idx.Type, i);

@@ -6407,39 +6433,39 @@ namespace Microsoft.Dafny
 

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr e = (SeqUpdateExpr)expr;

-        ResolveExpression(e.Seq, twoState, codeContext);

+        ResolveExpression(e.Seq, opts);

         Contract.Assert(e.Seq.Type != null);  // follows from postcondition of ResolveExpression

         Type elementType = new InferredTypeProxy();

         Type domainType = new InferredTypeProxy();

         Type rangeType = new InferredTypeProxy();

         if (UnifyTypes(e.Seq.Type, new SeqType(elementType))) {

-          ResolveExpression(e.Index, twoState, codeContext);

+          ResolveExpression(e.Index, opts);

           Contract.Assert(e.Index.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.Index.Type, Type.Int)) {

             Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type);

           }

-          ResolveExpression(e.Value, twoState, codeContext);

+          ResolveExpression(e.Value, opts);

           Contract.Assert(e.Value.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.Value.Type, elementType)) {

             Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);

           }

           expr.Type = e.Seq.Type;

         } else if (UnifyTypes(e.Seq.Type, new MapType(domainType, rangeType))) {

-          ResolveExpression(e.Index, twoState, codeContext);

+          ResolveExpression(e.Index, opts);

           if (!UnifyTypes(e.Index.Type, domainType)) {

             Error(e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);

           }

-          ResolveExpression(e.Value, twoState, codeContext);

+          ResolveExpression(e.Value, opts);

           if (!UnifyTypes(e.Value.Type, rangeType)) {

             Error(e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);

           }

           expr.Type = e.Seq.Type;

         } else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) {

-          ResolveExpression(e.Index, twoState, codeContext);

+          ResolveExpression(e.Index, opts);

           if (!UnifyTypes(e.Index.Type, elementType)) {

             Error(e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);

           }

-          ResolveExpression(e.Value, twoState, codeContext);

+          ResolveExpression(e.Value, opts);

           if (!UnifyTypes(e.Value.Type, Type.Int)) {

             Error(e.Value, "multiset update requires integer value (got {0})", e.Value.Type);

           }

@@ -6485,7 +6511,7 @@ namespace Microsoft.Dafny
                 }

 

                 DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

-                ResolveExpression(ctor_call, twoState, codeContext);

+                ResolveExpression(ctor_call, opts);

                 e.ResolvedUpdateExpr = ctor_call;

 

                 expr.Type = e.Seq.Type;

@@ -6498,13 +6524,13 @@ namespace Microsoft.Dafny
 

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        ResolveFunctionCallExpr(e, twoState, codeContext, false);

+        ResolveFunctionCallExpr(e, opts, false);

 

       } else if (expr is ApplyExpr) {

         ApplyExpr e = (ApplyExpr)expr;

-        ResolveExpression(e.Function, twoState, codeContext);

+        ResolveExpression(e.Function, opts);

         foreach (var arg in e.Args) {

-          ResolveExpression(arg, twoState, codeContext);

+          ResolveExpression(arg, opts);

         }

         Type tb = new InferredTypeProxy();

         var targs = e.Args.ConvertAll(arg => arg.Type);

@@ -6517,15 +6543,15 @@ namespace Microsoft.Dafny
 

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

-        if (!twoState) {

+        if (!opts.twoState) {

           Error(expr, "old expressions are not allowed in this context");

         }

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         expr.Type = e.E.Type;

 

       } else if (expr is MultiSetFormingExpr) {

         MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         if (!UnifyTypes(e.E.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {

           Error(e.tok, "can only form a multiset from a seq or set.");

         }

@@ -6533,7 +6559,7 @@ namespace Microsoft.Dafny
 

       } else if (expr is UnaryOpExpr) {

         var e = (UnaryOpExpr)expr;

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         switch (e.Op) {

           case UnaryOpExpr.Opcode.Not:

@@ -6549,7 +6575,7 @@ namespace Microsoft.Dafny
             expr.Type = Type.Int;

             break;

           case UnaryOpExpr.Opcode.Fresh:

-            if (!twoState) {

+            if (!opts.twoState) {

               Error(expr, "fresh expressions are not allowed in this context");

             }

             // the type of e.E must be either an object or a collection of objects

@@ -6576,7 +6602,7 @@ namespace Microsoft.Dafny
       } else if (expr is ConversionExpr) {

         var e = (ConversionExpr)expr;

         ResolveType(e.tok, e.ToType, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         if (e.ToType is IntType) {

           if (!(e.E.Type.IsRealType)) {

             Error(expr, "type conversion to int is allowed only from real (got {0})", e.E.Type);

@@ -6592,9 +6618,9 @@ namespace Microsoft.Dafny
 

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

-        ResolveExpression(e.E0, twoState, codeContext);

+        ResolveExpression(e.E0, opts);

         Contract.Assert(e.E0.Type != null);  // follows from postcondition of ResolveExpression

-        ResolveExpression(e.E1, twoState, codeContext);

+        ResolveExpression(e.E1, opts);

         Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

         switch (e.Op) {

           case BinaryExpr.Opcode.Iff:

@@ -6755,9 +6781,9 @@ namespace Microsoft.Dafny
 

       } else if (expr is TernaryExpr) {

         var e = (TernaryExpr)expr;

-        ResolveExpression(e.E0, twoState, codeContext);

-        ResolveExpression(e.E1, twoState, codeContext);

-        ResolveExpression(e.E2, twoState, codeContext);

+        ResolveExpression(e.E0, opts);

+        ResolveExpression(e.E1, opts);

+        ResolveExpression(e.E2, opts);

         switch (e.Op) {

           case TernaryExpr.Opcode.PrefixEqOp:

           case TernaryExpr.Opcode.PrefixNeqOp:

@@ -6781,7 +6807,7 @@ namespace Microsoft.Dafny
         var e = (LetExpr)expr;

         if (e.Exact) {

           foreach (var rhs in e.RHSs) {

-            ResolveExpression(rhs, twoState, codeContext);

+            ResolveExpression(rhs, opts);

           }

           scope.PushMarker();

           if (e.LHSs.Count != e.RHSs.Count) {

@@ -6821,20 +6847,20 @@ namespace Microsoft.Dafny
             ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);

           }

           foreach (var rhs in e.RHSs) {

-            ResolveExpression(rhs, twoState, codeContext);

+            ResolveExpression(rhs, opts);

             if (!UnifyTypes(rhs.Type, Type.Bool)) {

               Error(rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);

             }

           }

         }

-        ResolveExpression(e.Body, twoState, codeContext);

+        ResolveExpression(e.Body, opts);

         scope.PopMarker();

         expr.Type = e.Body.Type;

 

       } else if (expr is NamedExpr) {

         var e = (NamedExpr)expr;

-        ResolveExpression(e.Body, twoState, codeContext);

-        if (e.Contract != null) ResolveExpression(e.Contract, twoState, codeContext);

+        ResolveExpression(e.Body, opts);

+        if (e.Contract != null) ResolveExpression(e.Contract, opts);

         e.Type = e.Body.Type;

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

@@ -6855,20 +6881,20 @@ namespace Microsoft.Dafny
           Error(expr, "a quantifier cannot quantify over types. Possible fix: use the experimental attribute :typeQuantifier");

         }

         if (e.Range != null) {

-          ResolveExpression(e.Range, twoState, codeContext);

+          ResolveExpression(e.Range, opts);

           Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.Range.Type, Type.Bool)) {

             Error(expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);

           }

         }

-        ResolveExpression(e.Term, twoState, codeContext);

+        ResolveExpression(e.Term, opts);

         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.Term.Type, Type.Bool)) {

           Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);

         }

         // Since the body is more likely to infer the types of the bound variables, resolve it

         // first (above) and only then resolve the attributes (below).

-        ResolveAttributes(e.Attributes, twoState, codeContext);

+        ResolveAttributes(e.Attributes, opts);

         scope.PopMarker();

         allTypeParameters.PopMarker();

         expr.Type = Type.Bool;

@@ -6880,7 +6906,7 @@ namespace Microsoft.Dafny
           if (missingBounds.Count != 0) {

             // Report errors here about quantifications that depend on the allocation state.

             var mb = missingBounds;

-            if (codeContext is Function) {

+            if (opts.codeContext is Function) {

               mb = new List<BoundVar>();  // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)

               foreach (var bv in missingBounds) {

                 if (bv.Type.IsRefType) {

@@ -6906,15 +6932,15 @@ namespace Microsoft.Dafny
           }

           ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

-        ResolveExpression(e.Range, twoState, codeContext);

+        ResolveExpression(e.Range, opts);

         Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.Range.Type, Type.Bool)) {

           Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);

         }

-        ResolveExpression(e.Term, twoState, codeContext);

+        ResolveExpression(e.Term, opts);

         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

 

-        ResolveAttributes(e.Attributes, twoState, codeContext);

+        ResolveAttributes(e.Attributes, opts);

         scope.PopMarker();

         expr.Type = new SetType(e.Term.Type);

 

@@ -6924,8 +6950,8 @@ namespace Microsoft.Dafny
           e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

-            if (codeContext.IsGhost && (e.Term.Type.IsRefType || e.Term.Type is BoolType)) {

-              // ok!

+            if (opts.IsGhost && (e.Term.Type.IsRefType || e.Term.Type is BoolType)) {

+              // ok, term type is finite and we're in a ghost context

             } else {

               foreach (var bv in e.MissingBounds) {

                 Error(expr, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

@@ -6947,15 +6973,15 @@ namespace Microsoft.Dafny
           }

           ResolveType(v.tok, v.Type, ResolveTypeOptionEnum.InferTypeProxies, null);

         }

-        ResolveExpression(e.Range, twoState, codeContext);

+        ResolveExpression(e.Range, opts);

         Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.Range.Type, Type.Bool)) {

           Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);

         }

-        ResolveExpression(e.Term, twoState, codeContext);

+        ResolveExpression(e.Term, opts);

         Contract.Assert(e.Term.Type != null);  // follows from postcondition of ResolveExpression

 

-        ResolveAttributes(e.Attributes, twoState, codeContext);

+        ResolveAttributes(e.Attributes, opts);

         scope.PopMarker();

         expr.Type = new MapType(e.BoundVars[0].Type, e.Term.Type);

 

@@ -6982,7 +7008,7 @@ namespace Microsoft.Dafny
         }

 

         if (e.Range != null) {

-          ResolveExpression(e.Range, twoState, codeContext);

+          ResolveExpression(e.Range, opts);

           Contract.Assert(e.Range.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.Range.Type, Type.Bool)) {

             Error(expr, "Precondition must be boolean (got {0})", e.Range.Type);

@@ -6990,10 +7016,10 @@ namespace Microsoft.Dafny
         }

 

         foreach (var read in e.Reads) {

-          ResolveFrameExpression(read, "reads", false, codeContext);

+          ResolveFrameExpression(read, "reads", false, opts.codeContext);

         }

 

-        ResolveExpression(e.Term, twoState, codeContext);

+        ResolveExpression(e.Term, opts);

         Contract.Assert(e.Term.Type != null);

         scope.PopMarker();

         expr.Type = new ArrowType(Util.Map(e.BoundVars, v => v.Type), e.Body.Type);

@@ -7002,7 +7028,7 @@ namespace Microsoft.Dafny
       } else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

         int prevErrorCount = ErrorCount;

-        ResolveStatement(e.S, true, codeContext);

+        ResolveStatement(e.S, true, opts.codeContext);

         if (ErrorCount == prevErrorCount) {

           var r = e.S as UpdateStmt;

           if (r != null && r.ResolvedStatements.Count == 1) {

@@ -7012,17 +7038,17 @@ namespace Microsoft.Dafny
             }

           }

         }

-        ResolveExpression(e.E, twoState, codeContext);

+        ResolveExpression(e.E, opts);

         Contract.Assert(e.E.Type != null);  // follows from postcondition of ResolveExpression

         expr.Type = e.E.Type;

 

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

-        ResolveExpression(e.Test, twoState, codeContext);

+        ResolveExpression(e.Test, opts);

         Contract.Assert(e.Test.Type != null);  // follows from postcondition of ResolveExpression

-        ResolveExpression(e.Thn, twoState, codeContext);

+        ResolveExpression(e.Thn, opts);

         Contract.Assert(e.Thn.Type != null);  // follows from postcondition of ResolveExpression

-        ResolveExpression(e.Els, twoState, codeContext);

+        ResolveExpression(e.Els, opts);

         Contract.Assert(e.Els.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.Test.Type, Type.Bool)) {

           Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);

@@ -7035,7 +7061,7 @@ namespace Microsoft.Dafny
 

       } else if (expr is MatchExpr) {

         var me = (MatchExpr)expr;

-        ResolveExpression(me.Source, twoState, codeContext);

+        ResolveExpression(me.Source, opts);

         Contract.Assert(me.Source.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

         DatatypeDecl dtd = null;

@@ -7097,7 +7123,7 @@ namespace Microsoft.Dafny
             }

             i++;

           }

-          ResolveExpression(mc.Body, twoState, codeContext);

+          ResolveExpression(mc.Body, opts);

           Contract.Assert(mc.Body.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(expr.Type, mc.Body.Type)) {

             Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);

@@ -7186,7 +7212,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    private void ResolveDatatypeValue(bool twoState, ICodeContext codeContext, DatatypeValue dtv, DatatypeDecl dt) {

+    private void ResolveDatatypeValue(ResolveOpts opts, DatatypeValue dtv, DatatypeDecl dt) {

       // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)

       List<Type> gt = new List<Type>(dt.TypeArgs.Count);

       Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

@@ -7212,7 +7238,7 @@ namespace Microsoft.Dafny
       int j = 0;

       foreach (Expression arg in dtv.Arguments) {

         Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

-        ResolveExpression(arg, twoState, codeContext);

+        ResolveExpression(arg, opts);

         Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

         if (formal != null) {

           Type st = SubstType(formal.Type, subst);

@@ -7438,8 +7464,8 @@ namespace Microsoft.Dafny
     /// Otherwise (that is, if "allowMethodCall" and what is being called refers to a method), resolves the receiver

     /// of "e" but NOT the arguments, and returns a CallRhs corresponding to the call.

     /// </summary>

-    public CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, bool twoState, ICodeContext codeContext, bool allowMethodCall) {

-      ResolveReceiver(e.Receiver, twoState, codeContext);

+    public CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, ResolveOpts opts, bool allowMethodCall) {

+      ResolveReceiver(e.Receiver, opts);

       Contract.Assert(e.Receiver.Type != null);  // follows from postcondition of ResolveExpression

       NonProxyType nptype;

 

@@ -7496,7 +7522,7 @@ namespace Microsoft.Dafny
           // type check the arguments

           for (int i = 0; i < function.Formals.Count; i++) {

             Expression farg = e.Args[i];

-            ResolveExpression(farg, twoState, codeContext);

+            ResolveExpression(farg, opts);

             Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression

             Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);

             if (!UnifyTypes(farg.Type, s)) {

@@ -7506,7 +7532,7 @@ namespace Microsoft.Dafny
           e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);

         }

 

-        AddCallGraphEdge(e, codeContext, function);

+        AddCallGraphEdge(e, opts.codeContext, function);

       }

       return null;

     }

@@ -7541,7 +7567,7 @@ namespace Microsoft.Dafny
     /// If "!allowMethodCall", or if "e" does not designate a method call, resolves "e" and returns "null".

     /// Otherwise, resolves all sub-parts of "e" and returns a (resolved) CallRhs expression representing the call.

     /// </summary>

-    CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, ICodeContext codeContext, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequence(IdentifierSequence e, ResolveOpts opts, bool allowMethodCall) {

       // Look up "id" as follows:

       //  - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)

       //  - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)

@@ -7562,8 +7588,8 @@ namespace Microsoft.Dafny
       if (scope.Find(id.val) != null) {

         // ----- root is a local variable, parameter, or bound variable

         r = new IdentifierExpr(id, id.val);

-        ResolveExpression(r, twoState, codeContext);

-        r = ResolveSuffix(r, e, 1, twoState, codeContext, allowMethodCall, out call);

+        ResolveExpression(r, opts);

+        r = ResolveSuffix(r, e, 1, opts, allowMethodCall, out call);

 

       } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

@@ -7578,27 +7604,27 @@ namespace Microsoft.Dafny
           Error(id, "name of type ('{0}') is used as a function", id.val);

           // resolve the arguments nonetheless

           foreach (var arg in e.Arguments) {

-            ResolveExpression(arg, twoState, codeContext);

+            ResolveExpression(arg, opts);

           }

         } else if (decl is ClassDecl) {

           // ----- root is a class

           var cd = (ClassDecl)decl;

-          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, codeContext, allowMethodCall, out call);

+          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, opts, allowMethodCall, out call);

 

         } else if (decl is ModuleDecl) {

           // ----- root is a submodule

           if (!(1 < e.Tokens.Count)) {

             Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);

           }

-          call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, twoState, codeContext, allowMethodCall);

+          call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);

         } else {

           // ----- root is a datatype

           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

           var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

-          ResolveExpression(r, twoState, codeContext);

+          ResolveExpression(r, opts);

           if (e.Tokens.Count != 2) {

-            r = ResolveSuffix(r, e, 2, twoState, codeContext, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, 2, opts, allowMethodCall, out call);

           }

         }

 

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

           var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);

-          ResolveExpression(r, twoState, codeContext);

+          ResolveExpression(r, opts);

           if (e.Tokens.Count != 1) {

-            r = ResolveSuffix(r, e, 1, twoState, codeContext, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, 1, opts, allowMethodCall, out call);

           }

         }

 

@@ -7635,7 +7661,7 @@ namespace Microsoft.Dafny
             receiver = new ImplicitThisExpr(id);

             receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass);  // resolve here

           }

-          r = ResolveSuffix(receiver, e, 0, twoState, codeContext, allowMethodCall, out call);

+          r = ResolveSuffix(receiver, e, 0, opts, allowMethodCall, out call);

         }

 

       } else {

@@ -7643,7 +7669,7 @@ namespace Microsoft.Dafny
         // resolve arguments, if any

         if (e.Arguments != null) {

           foreach (var arg in e.Arguments) {

-            ResolveExpression(arg, twoState, codeContext);

+            ResolveExpression(arg, opts);

           }

         }

       }

@@ -7655,7 +7681,7 @@ namespace Microsoft.Dafny
       return call;

     }

 

-    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, ICodeContext codeContext, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, ResolveOpts opts, bool allowMethodCall) {

       // Look up "id" as follows:

       //  - unambiguous type/module name (class, datatype, sub-module (including submodules of imports) or opaque type)

       //       (if two imported types have the same name, an error message is produced here)

@@ -7679,22 +7705,22 @@ namespace Microsoft.Dafny
           if (!(p + 1 < e.Tokens.Count)) {

             Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);

           }

-          call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, codeContext, allowMethodCall);

+          call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, opts, allowMethodCall);

         } else if (decl is TypeSynonymDecl) {

           // ----- root apparently refers to a type synonym

           Error(e.tok, "type synonym {0} cannot be used here", id.val);  // todo: this is a bit of a cop-out; perhaps something better could be done

         } else if (decl is ClassDecl) {

           // ----- root is a class

           var cd = (ClassDecl)decl;

-          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, twoState, codeContext, allowMethodCall, out call);

+          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, opts, allowMethodCall, out call);

         } else {

           // ----- root is a datatype

           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

           var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);

-          ResolveDatatypeValue(twoState, codeContext, (DatatypeValue)r, dt);

+          ResolveDatatypeValue(opts, (DatatypeValue)r, dt);

           if (e.Tokens.Count != p + 2) {

-            r = ResolveSuffix(r, e, p + 2, twoState, codeContext, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, p + 2, opts, allowMethodCall, out call);

           }

         }

       } else if (sig.Ctors.TryGetValue(id.val, out pair)) {

@@ -7706,9 +7732,9 @@ namespace Microsoft.Dafny
           var dt = pair.Item1.EnclosingDatatype;

           var args = (e.Tokens.Count == p + 1 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, dt.Name, id.val, args);

-          ResolveDatatypeValue(twoState, codeContext, (DatatypeValue)r, dt);

+          ResolveDatatypeValue(opts, (DatatypeValue)r, dt);

           if (e.Tokens.Count != p + 1) {

-            r = ResolveSuffix(r, e, p + 1, twoState, codeContext, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, p + 1, opts, allowMethodCall, out call);

           }

         }

       } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

@@ -7717,14 +7743,14 @@ namespace Microsoft.Dafny
         Expression receiver;

         Contract.Assert(member.IsStatic);

         receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

-        r = ResolveSuffix(receiver, e, p, twoState, codeContext, allowMethodCall, out call);

+        r = ResolveSuffix(receiver, e, p, opts, allowMethodCall, out call);

 

       } else {

         Error(id, "unresolved identifier: {0}", id.val);

         // resolve arguments, if any

         if (e.Arguments != null) {

           foreach (var arg in e.Arguments) {

-            ResolveExpression(arg, twoState, codeContext);

+            ResolveExpression(arg, opts);

           }

         }

       }

@@ -7750,7 +7776,7 @@ namespace Microsoft.Dafny
     /// Except, if "allowMethodCall" is "true" and the would-be-returned value designates a method

     /// call, instead returns null and returns "call" as a non-null value.

     /// </summary>

-    Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, ICodeContext codeContext, bool allowMethodCall, out CallRhs call) {

+    Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, ResolveOpts opts, bool allowMethodCall, out CallRhs call) {

       Contract.Requires(r != null);

       Contract.Requires(e != null);

       Contract.Requires(0 <= p && p <= e.Tokens.Count);

@@ -7763,7 +7789,7 @@ namespace Microsoft.Dafny
         var resolved = ResolveMemberSelect(e.Tokens[p], r, e.Tokens[p].val);

         if (resolved != null) {

           r = resolved;

-          ResolveExpression(r, twoState, codeContext);

+          ResolveExpression(r, opts);

         }

       }

 

@@ -7792,18 +7818,18 @@ namespace Microsoft.Dafny
           r = null;

         } else {

           r = NewFunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.OpenParen, e.Arguments);

-          ResolveExpression(r, twoState, codeContext);

+          ResolveExpression(r, opts);

         }

       } else if (e.Arguments != null) {

         Contract.Assert(p == e.Tokens.Count);

         if (r.Type is ArrowType || r.Type.IsTypeParameter) {

           r = new ApplyExpr(e.tok, e.OpenParen, r, e.Arguments);

-          ResolveExpression(r, twoState, codeContext);

+          ResolveExpression(r, opts);

         } else {

           Error(e.OpenParen, "non-function expression is called with parameters");

           // resolve the arguments nonetheless

           foreach (var arg in e.Arguments) {

-            ResolveExpression(arg, twoState, codeContext);

+            ResolveExpression(arg, opts);

           }

         }

       } 

@@ -8314,7 +8340,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    void ResolveReceiver(Expression expr, bool twoState, ICodeContext codeContext) {

+    void ResolveReceiver(Expression expr, ResolveOpts opts) {

       Contract.Requires(expr != null);

       Contract.Ensures(expr.Type != null);

 

@@ -8324,11 +8350,11 @@ namespace Microsoft.Dafny
         Contract.Assume(currentClass != null);  // this is really a precondition, in this case

         expr.Type = GetThisType(expr.tok, currentClass);

       } else {

-        ResolveExpression(expr, twoState, codeContext);

+        ResolveExpression(expr, opts);

       }

     }

 

-    void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, ICodeContext codeContext, bool allowNonUnitArraySelection) {

+    void ResolveSeqSelectExpr(SeqSelectExpr e, ResolveOpts opts, bool allowNonUnitArraySelection) {

       Contract.Requires(e != null);

       if (e.Type != null) {

         // already resolved

@@ -8336,7 +8362,7 @@ namespace Microsoft.Dafny
       }

 

       bool seqErr = false;

-      ResolveExpression(e.Seq, twoState, codeContext);

+      ResolveExpression(e.Seq, opts);

       Contract.Assert(e.Seq.Type != null);  // follows from postcondition of ResolveExpression

       Type elementType = new InferredTypeProxy();

       Type domainType = new InferredTypeProxy();

@@ -8361,14 +8387,14 @@ namespace Microsoft.Dafny
         }

       }

       if (e.E0 != null) {

-        ResolveExpression(e.E0, twoState, codeContext);

+        ResolveExpression(e.E0, opts);

         Contract.Assert(e.E0.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E0.Type, domainType)) {

           Error(e.E0, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E0.Type, domainType);

         }

       }

       if (e.E1 != null) {

-        ResolveExpression(e.E1, twoState, codeContext);

+        ResolveExpression(e.E1, opts);

         Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(e.E1.Type, domainType)) {

           Error(e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domainType);

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 9f6c948a..50628438 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -373,7 +373,7 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
     n + m; // error: ==> operator requires boolean lines

     n + m + 1;

     n + m + 2;

-  }    

+  }

   calc {

     n + m;

     n + m + 1;

@@ -394,8 +394,8 @@ ghost method Mod(a: int)
   ensures ycalc == a;

 {

   ycalc := a;

-}  

-  

+}

+

 ghost method Bad()

   modifies this;

   ensures 0 == 1;

@@ -465,7 +465,7 @@ method AssignSuchThatFromGhost()
   ghost var g: int;

 

   x := g;  // error: ghost cannot flow into non-ghost

-  

+

   x := *;

   assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,

                   // the compiler will complain)

@@ -509,7 +509,7 @@ module NoTypeArgs0 {
     match t

     case Leaf(_,_) => t

     case Node(x, y) => x

-  }  

+  }

 

   function FTree1(t: Tree): Tree

   {

@@ -1100,3 +1100,17 @@ method TraitSynonym()
 {

   var x := new JJ;  // error: new cannot be applied to a trait

 }

+

+// ----- set comprehensions where the term type is finite ----

+

+module ObjectSetComprehensions {

+  // allowed in non-ghost context:

+  function A() : set<object> { set o : object | true :: o }

+

+  lemma B() { var x := set o : object | true :: o; }

+

+  // not allowed in non-ghost context:

+  function method C() : set<object> { set o : object | true :: o }

+

+  method D() { var x := set o : object | true :: o; }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b11fa9f8..ac44375d 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -76,6 +76,8 @@ ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)

 ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)

 ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)

+ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

+ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

 ResolutionErrors.dfy(429,2): Error: More than one default constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

@@ -173,4 +175,4 @@ ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from
 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

-175 resolution/type errors detected in ResolutionErrors.dfy

+177 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index 47f7f575..d0a8b43b 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -101,3 +101,33 @@ module WhatWeKnowAboutReads {
     }
   }
 }
+
+module ReadsAll {
+  function A(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method B(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function C(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method D(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+}
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index e83e017c..f1da2003 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -36,4 +36,4 @@ Execution trace:
     ReadsReads.dfy(95,16): anon15_Else

     (0,0): anon21_Then

 

-Dafny program verifier finished with 13 verified, 9 errors

+Dafny program verifier finished with 17 verified, 9 errors