Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

8 files changed, 218 insertions, 194 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9f2feb14..1c376c49 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1336,11 +1336,6 @@ namespace Microsoft.Dafny
       // ---------------------------------- Pass 0 ----------------------------------

       // This pass resolves names, introduces (and may solve) type constraints, and

       // builds the module's call graph.

-      // Some bounds are discovered during this pass [is this necessary? can they be

-      // moved to pass 1 like the other bounds discovery? --KRML], namely:

-      //   - forall statements

-      //   - quantifier expressions

-      //   - map comprehensions

       // For 'newtype' declarations, it also checks that all types were fully

       // determined.

       // ----------------------------------------------------------------------------

@@ -1375,7 +1370,7 @@ namespace Microsoft.Dafny
             if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) {

               reporter.Error(MessageSource.Resolver, dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);

             }

-            CheckTypeInference(dd.Constraint);

+            CheckTypeInference(dd.Constraint, dd);

             scope.PopMarker();

           }

         }

@@ -1408,7 +1403,10 @@ namespace Microsoft.Dafny
       // * checks that type inference was able to determine all types

       // * fills in the .ResolvedOp field of binary expressions

       // * discovers bounds for:

+      //     - forall statements

       //     - set comprehensions

+      //     - map comprehensions

+      //     - quantifier expressions

       //     - assign-such-that statements

       //     - compilable let-such-that expressions

       //     - newtype constraints

@@ -1432,7 +1430,7 @@ namespace Microsoft.Dafny
               iter.SubExpressions.Iter(e => CheckExpression(e, this, iter));

             }

             if (iter.Body != null) {

-              CheckTypeInference(iter.Body);

+              CheckTypeInference(iter.Body, iter);

               if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {

                 ComputeGhostInterest(iter.Body, false, iter);

                 CheckExpression(iter.Body, this, iter);

@@ -2047,22 +2045,22 @@ namespace Microsoft.Dafny
     private void CheckTypeInference_Member(MemberDecl member) {

       if (member is Method) {

         var m = (Method)member;

-        m.Req.Iter(CheckTypeInference_MaybeFreeExpression);

-        m.Ens.Iter(CheckTypeInference_MaybeFreeExpression);

-        CheckTypeInference_Specification_FrameExpr(m.Mod);

-        CheckTypeInference_Specification_Expr(m.Decreases);

+        m.Req.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));

+        m.Ens.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));

+        CheckTypeInference_Specification_FrameExpr(m.Mod, m);

+        CheckTypeInference_Specification_Expr(m.Decreases, m);

         if (m.Body != null) {

-          CheckTypeInference(m.Body);

+          CheckTypeInference(m.Body, m);

         }

       } else if (member is Function) {

         var f = (Function)member;

         var errorCount = reporter.Count(ErrorLevel.Error);

-        f.Req.Iter(CheckTypeInference);

-        f.Ens.Iter(CheckTypeInference);

-        f.Reads.Iter(fe => CheckTypeInference(fe.E));

-        CheckTypeInference_Specification_Expr(f.Decreases);

+        f.Req.Iter(e => CheckTypeInference(e, f));

+        f.Ens.Iter(e => CheckTypeInference(e, f));

+        f.Reads.Iter(fe => CheckTypeInference(fe.E, f));

+        CheckTypeInference_Specification_Expr(f.Decreases, f);

         if (f.Body != null) {

-          CheckTypeInference(f.Body);

+          CheckTypeInference(f.Body, f);

         }

         if (errorCount == reporter.Count(ErrorLevel.Error) && f is FixpointPredicate) {

           var cop = (FixpointPredicate)f;

@@ -2071,43 +2069,51 @@ namespace Microsoft.Dafny
       }

     }

 

-    private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe) {

+    private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe, ICodeContext codeContext) {

       Contract.Requires(mfe != null);

+      Contract.Requires(codeContext != null);

       foreach (var e in Attributes.SubExpressions(mfe.Attributes)) {

-        CheckTypeInference(e);

+        CheckTypeInference(e, codeContext);

       }

-      CheckTypeInference(mfe.E);

+      CheckTypeInference(mfe.E, codeContext);

     }

-    private void CheckTypeInference_Specification_Expr(Specification<Expression> spec) {

+    private void CheckTypeInference_Specification_Expr(Specification<Expression> spec, ICodeContext codeContext) {

       Contract.Requires(spec != null);

+      Contract.Requires(codeContext != null);

       foreach (var e in Attributes.SubExpressions(spec.Attributes)) {

-        CheckTypeInference(e);

+        CheckTypeInference(e, codeContext);

       }

-      spec.Expressions.Iter(CheckTypeInference);

+      spec.Expressions.Iter(e => CheckTypeInference(e, codeContext));

     }

-    private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec) {

+    private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec, ICodeContext codeContext) {

       Contract.Requires(spec != null);

+      Contract.Requires(codeContext != null);

       foreach (var e in Attributes.SubExpressions(spec.Attributes)) {

-        CheckTypeInference(e);

+        CheckTypeInference(e, codeContext);

       }

-      spec.Expressions.Iter(fe => CheckTypeInference(fe.E));

+      spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext));

     }

-    void CheckTypeInference(Expression expr) {

+    void CheckTypeInference(Expression expr, ICodeContext codeContext) {

       Contract.Requires(expr != null);

+      Contract.Requires(codeContext != null);

       PartiallySolveTypeConstraints();

-      var c = new CheckTypeInference_Visitor(this);

+      var c = new CheckTypeInference_Visitor(this, codeContext);

       c.Visit(expr);

     }

-    void CheckTypeInference(Statement stmt) {

+    void CheckTypeInference(Statement stmt, ICodeContext codeContext) {

       Contract.Requires(stmt != null);

-      var c = new CheckTypeInference_Visitor(this);

+      Contract.Requires(codeContext != null);

+      var c = new CheckTypeInference_Visitor(this, codeContext);

       c.Visit(stmt);

     }

     class CheckTypeInference_Visitor : ResolverBottomUpVisitor

     {

-      public CheckTypeInference_Visitor(Resolver resolver)

+      readonly ICodeContext codeContext;

+      public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext)

         : base(resolver) {

         Contract.Requires(resolver != null);

+        Contract.Requires(codeContext != null);

+        this.codeContext = codeContext;

       }

       protected override void VisitOneStmt(Statement stmt) {

         if (stmt is VarDeclStmt) {

@@ -2118,6 +2124,9 @@ namespace Microsoft.Dafny
         } else if (stmt is ForallStmt) {

           var s = (ForallStmt)stmt;

           s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));

+          List<BoundVar> missingBounds;

+          s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);

+

         } else if (stmt is AssignSuchThatStmt) {

           var s = (AssignSuchThatStmt)stmt;

           if (s.AssumeToken == null) {

@@ -2154,27 +2163,55 @@ namespace Microsoft.Dafny
               resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name);

             }

           }

-          if (e is SetComprehension) {

-            var sc = (SetComprehension)e;

-            if (sc.Finite) {

-              // A set must be finite.  Discover bounds for the Range expression, but report an error only if the Term is not

-              // of a finite-individuals type.

-              List<BoundVar> missingBounds;

-              sc.Bounds = DiscoverBestBounds_MultipleVars(sc.BoundVars, sc.Range, true, true, out missingBounds);

-              if (missingBounds.Count != 0) {

-                sc.MissingBounds = missingBounds;

-                if (sc.Type.HasFinitePossibleValues) {

-                  // This means the set is finite, regardless of if the Range is bounded.  So, we don't give any error here.

-                  // However, if this expression is used in a non-ghost context (which is not yet known at this stage of

-                  // resolution), the resolver will generate an error about that later.

-                } else {

-                  foreach (var bv in sc.MissingBounds) {

-                    resolver.reporter.Error(MessageSource.Resolver, sc, "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);

-                  }

+          // apply bounds discovery to quantifiers, finite sets, and finite maps

+          string what = null;

+          Expression whereToLookForBounds = null;

+          bool polarity = true;

+          if (e is QuantifierExpr) {

+            what = "quantifier";

+            whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();

+            polarity = e is ExistsExpr;

+          } else if (e is SetComprehension && ((SetComprehension)e).Finite) {

+            what = "set comprehension";

+            whereToLookForBounds = e.Range;

+          } else if (e is MapComprehension && ((MapComprehension)e).Finite) {

+            what = "map comprehension";

+            whereToLookForBounds = e.Range;

+          }

+          if (whereToLookForBounds != null) {

+            List<BoundVar> missingBounds;

+            e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, whereToLookForBounds, polarity, true, out missingBounds);

+            if (missingBounds.Count != 0) {

+              e.MissingBounds = missingBounds;

+

+              if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {

+                // a possibly infinite set/map has no restrictions on its range

+              } else if (e is QuantifierExpr) {

+                // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)

+              } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {

+                // This means the set is finite, regardless of if the Range is bounded.  So, we don't give any error here.

+                // However, if this expression is used in a non-ghost context (which is not yet known at this stage of

+                // resolution), the resolver will generate an error about that later.

+              } else {

+                // we cannot be sure that the set/map really is finite

+                foreach (var bv in missingBounds) {

+                  resolver.reporter.Error(MessageSource.Resolver, e, "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name);

+                }

+              }

+            }

+            if (codeContext is Function && e.Bounds != null) {

+              // functions are not allowed to depend on the set of allocated objects

+              Contract.Assert(e.Bounds.Count == e.BoundVars.Count);

+              for (int i = 0; i < e.Bounds.Count; i++) {

+                var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;

+                if (bound != null) {

+                  var bv = e.BoundVars[i];

+                  resolver.reporter.Error(MessageSource.Resolver, expr, "a {0} involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{1}'", what, bv.Name);

                 }

               }

             }

           }

+

         } else if (expr is MemberSelectExpr) {

           var e = (MemberSelectExpr)expr;

           if (e.Member is Function || e.Member is Method) {

@@ -4035,7 +4072,7 @@ namespace Microsoft.Dafny
             int prevErrors = reporter.Count(ErrorLevel.Error);

             ResolveExpression(arg, opts);

             if (prevErrors == reporter.Count(ErrorLevel.Error)) {

-              CheckTypeInference(arg);

+              CheckTypeInference(arg, opts.codeContext);

             }

           }

         }

@@ -4289,7 +4326,7 @@ namespace Microsoft.Dafny
             scope.Push(k.Name, k);  // we expect no name conflict for _k

           }

           var prevErrorCount = reporter.Count(ErrorLevel.Error);

-          ResolveBlockStatement(m.Body, m.IsGhost, m);

+          ResolveBlockStatement(m.Body, m);

           SolveAllTypeConstraints();

           if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {

 //KRML            ComputeGhostInterest(m.Body, m);

@@ -4411,7 +4448,7 @@ namespace Microsoft.Dafny
 

       // Resolve body

       if (iter.Body != null) {

-        ResolveBlockStatement(iter.Body, false, iter);

+        ResolveBlockStatement(iter.Body, iter);

         if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {

           //KRML          ComputeGhostInterest(iter.Body, iter);

         }

@@ -5249,11 +5286,7 @@ namespace Microsoft.Dafny
       return at;

     }

 

-    /// <summary>

-    /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it

-    /// at run time.  That means it must not have any side effects on non-ghost variables, for example.

-    /// </summary>

-    public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {

+    public void ResolveStatement(Statement stmt, ICodeContext codeContext) {

       Contract.Requires(stmt != null);

       Contract.Requires(codeContext != null);

       if (!(stmt is ForallStmt)) {  // forall statements do their own attribute resolution below

@@ -5328,13 +5361,13 @@ namespace Microsoft.Dafny
             }

             s.hiddenUpdate = new UpdateStmt(s.Tok, s.EndTok, formals, s.rhss, true);

             // resolving the update statement will check for return/yield statement specifics.

-            ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext);

+            ResolveStatement(s.hiddenUpdate, codeContext);

           }

         } else {// this is a regular return/yield statement.

           s.hiddenUpdate = null;

         }

       } else if (stmt is ConcreteUpdateStatement) {

-        ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);

+        ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, codeContext);

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

         // We have three cases.

@@ -5370,7 +5403,7 @@ namespace Microsoft.Dafny
             lhs.Type = local.Type;

           }

           // resolve the whole thing

-          ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

+          ResolveConcreteUpdateStmt(s.Update, codeContext);

         }

         // Add the locals to the scope

         foreach (var local in s.Locals) {

@@ -5382,7 +5415,7 @@ namespace Microsoft.Dafny
         }

         // Resolve the AssignSuchThatStmt, if any

         if (s.Update is AssignSuchThatStmt) {

-          ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);

+          ResolveConcreteUpdateStmt(s.Update, codeContext);

         }

         // Update the VarDeclStmt's ghost status according to its components

         foreach (var local in s.Locals)

@@ -5481,52 +5514,40 @@ namespace Microsoft.Dafny
       } else if (stmt is BlockStmt) {

         var s = (BlockStmt)stmt;

         scope.PushMarker();

-        ResolveBlockStatement(s, specContextOnly, codeContext);

+        ResolveBlockStatement(s, codeContext);

         scope.PopMarker();

 

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

-        bool branchesAreSpecOnly = specContextOnly;

         if (s.Guard != null) {

-          int prevErrorCount = reporter.Count(ErrorLevel.Error);

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

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

-          bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;

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

-          if (!specContextOnly && successfullyResolved) {

-            branchesAreSpecOnly = UsesSpecFeatures(s.Guard);

-          }

         }

-        ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext);

+        ResolveStatement(s.Thn, codeContext);

         if (s.Els != null) {

-          ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);

+          ResolveStatement(s.Els, codeContext);

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);

+        ResolveAlternatives(s.Alternatives, null, codeContext);

 

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

-        bool bodyMustBeSpecOnly = specContextOnly;

         var fvs = new HashSet<IVariable>();

         if (s.Guard != null) {

-          int prevErrorCount = reporter.Count(ErrorLevel.Error);

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

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

-          bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;

           Translator.ComputeFreeVariables(s.Guard, fvs);

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

-          if (!specContextOnly && successfullyResolved) {

-            bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard);

-          }

         }

 

         ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs);

 

         if (s.Body != null) {

           loopStack.Add(s);  // push

-          ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

+          ResolveStatement(s.Body, codeContext);

           loopStack.RemoveAt(loopStack.Count - 1);  // pop

         } else {

           string text = "havoc {" + Util.Comma(", ", fvs, fv => fv.Name) + "};";  // always terminate with a semi-colon

@@ -5535,7 +5556,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

-        ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);

+        ResolveAlternatives(s.Alternatives, s, codeContext);

         ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, null);

 

       } else if (stmt is ForallStmt) {

@@ -5559,23 +5580,13 @@ namespace Microsoft.Dafny
         // first (above) and only then resolve the attributes (below).

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

 

-        bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == reporter.Count(ErrorLevel.Error) && UsesSpecFeatures(s.Range));

-        if (!bodyMustBeSpecOnly && prevErrorCount == reporter.Count(ErrorLevel.Error)) {

-          CheckTypeInference(s.Range);  // we need to resolve operators before the call to DiscoverBounds

-          List<BoundVar> missingBounds;

-          s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);

-          if (missingBounds.Count != 0) {

-            bodyMustBeSpecOnly = true;

-          }

-        }

-

         if (s.Body != null) {

           // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement

           var prevLblStmts = labeledStatements;

           var prevLoopStack = loopStack;

           labeledStatements = new Scope<Statement>();

           loopStack = new List<Statement>();

-          ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);

+          ResolveStatement(s.Body, codeContext);

           labeledStatements = prevLblStmts;

           loopStack = prevLoopStack;

         }

@@ -5627,7 +5638,7 @@ namespace Microsoft.Dafny
           ResolveFrameExpression(fe, false, codeContext);

         }

         if (s.Body != null) {

-          ResolveBlockStatement(s.Body, specContextOnly, codeContext);

+          ResolveBlockStatement(s.Body, codeContext);

         }

 

       } else if (stmt is CalcStmt) {

@@ -5658,7 +5669,7 @@ namespace Microsoft.Dafny
           labeledStatements = new Scope<Statement>();

           loopStack = new List<Statement>();

           foreach (var h in s.Hints) {

-            ResolveStatement(h, true, codeContext);

+            ResolveStatement(h, codeContext);

           }

           labeledStatements = prevLblStmts;

           loopStack = prevLoopStack;

@@ -5675,13 +5686,13 @@ namespace Microsoft.Dafny
         Contract.Assert(prevErrorCount != reporter.Count(ErrorLevel.Error) || s.Steps.Count == s.Hints.Count);

 

       } else if (stmt is MatchStmt) {

-        ResolveMatchStmt(stmt, specContextOnly, codeContext);

+        ResolveMatchStmt(stmt, codeContext);

       } else if (stmt is SkeletonStatement) {

         var s = (SkeletonStatement)stmt;

         reporter.Error(MessageSource.Resolver, s.Tok, "skeleton statements are allowed only in refining methods");

         // nevertheless, resolve the underlying statement; hey, why not

         if (s.S != null) {

-          ResolveStatement(s.S, specContextOnly, codeContext);

+          ResolveStatement(s.S, codeContext);

         }

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

@@ -5726,18 +5737,12 @@ namespace Microsoft.Dafny
       }

     }

 

-    void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) {

+    void ResolveMatchStmt(Statement stmt, ICodeContext codeContext) {

       MatchStmt s = (MatchStmt)stmt;

       DesugarMatchStmtWithTupleExpression(s);

 

-      bool bodyIsSpecOnly = specContextOnly;

-      int prevErrorCount = reporter.Count(ErrorLevel.Error);

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

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

-      bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;

-      if (!specContextOnly && successfullyResolved) {

-        bodyIsSpecOnly = UsesSpecFeatures(s.Source);

-      }

       UserDefinedType sourceType = null;

       DatatypeDecl dtd = null;

       if (s.Source.Type.IsDatatype) {

@@ -5814,7 +5819,7 @@ namespace Microsoft.Dafny
           }

         }

         foreach (Statement ss in mc.Body) {

-          ResolveStatement(ss, bodyIsSpecOnly, codeContext);

+          ResolveStatement(ss, codeContext);

         }

         // substitute body to replace the case pat with v. This needs to happen

         // after the body is resolved so we can scope the bv correctly.

@@ -5824,7 +5829,7 @@ namespace Microsoft.Dafny
           foreach (Statement ss in mc.Body) {

             Statement clone = cloner.CloneStmt(ss);

             // resolve it again since we just cloned it.

-            ResolveStatement(clone, bodyIsSpecOnly, codeContext);

+            ResolveStatement(clone, codeContext);

             list.Add(clone);

           }

           mc.UpdateBody(list);

@@ -6242,7 +6247,7 @@ namespace Microsoft.Dafny
         reporter.Info(MessageSource.Resolver, loopStmt.Tok, s);

       }

     }

-    private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {

+    private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext codeContext) {

       Contract.Requires(codeContext != null);

 

       // First, resolve all LHS's and expression-looking RHS's.

@@ -6265,7 +6270,7 @@ namespace Microsoft.Dafny
         var suchThat = (AssignSuchThatStmt)s;  // this is the other possible subclass

         ResolveAssignSuchThatStmt(suchThat, codeContext);

       } else {

-        ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs);

+        ResolveUpdateStmt(update, codeContext, errorCountBeforeCheckingLhs);

       }

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

     }

@@ -6274,7 +6279,7 @@ namespace Microsoft.Dafny
     /// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during

     /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.

     /// </summary>

-    private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {

+    private void ResolveUpdateStmt(UpdateStmt update, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {

       Contract.Requires(update != null);

       Contract.Requires(codeContext != null);

       IToken firstEffectfulRhs = null;

@@ -6367,7 +6372,7 @@ namespace Microsoft.Dafny
       }

 

       foreach (var a in update.ResolvedStatements) {

-        ResolveStatement(a, specContextOnly, codeContext);

+        ResolveStatement(a, codeContext);

       }

     }

 

@@ -6393,7 +6398,7 @@ namespace Microsoft.Dafny
       ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);

     }

 

-    void ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {

+    void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {

       Contract.Requires(alternatives != null);

       Contract.Requires(codeContext != null);

 

@@ -6412,7 +6417,7 @@ namespace Microsoft.Dafny
       foreach (var alternative in alternatives) {

         scope.PushMarker();

         foreach (Statement ss in alternative.Body) {

-          ResolveStatement(ss, specContextOnly, codeContext);

+          ResolveStatement(ss, codeContext);

         }

         scope.PopMarker();

       }

@@ -6541,7 +6546,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) {

+    void ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) {

       Contract.Requires(blockStmt != null);

       Contract.Requires(codeContext != null);

 

@@ -6561,7 +6566,7 @@ namespace Microsoft.Dafny
             Contract.Assert(r == Scope<Statement>.PushResult.Success);  // since we just checked for duplicates, we expect the Push to succeed

           }

         }

-        ResolveStatement(ss, specContextOnly, codeContext);

+        ResolveStatement(ss, codeContext);

         labeledStatements.PopMarker();

       }

     }

@@ -7878,25 +7883,6 @@ namespace Microsoft.Dafny
         allTypeParameters.PopMarker();

         expr.Type = Type.Bool;

 

-        if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {

-          CheckTypeInference(e.LogicalBody());  // we need to resolve operators before the call to DiscoverBounds

-          List<BoundVar> missingBounds;

-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);

-          if (missingBounds.Count != 0) {

-            e.MissingBounds = missingBounds;

-          }

-          if (opts.codeContext is Function && e.Bounds != null) {

-            Contract.Assert(e.Bounds.Count == e.BoundVars.Count);

-            for (int i = 0; i < e.Bounds.Count; i++) {

-              var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;

-              if (bound != null) {

-                var bv = e.BoundVars[i];

-                reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);

-              }

-            }

-          }

-        }

-

       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

@@ -7936,19 +7922,6 @@ namespace Microsoft.Dafny
         scope.PopMarker();

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

 

-        if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {

-          CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds

-          List<BoundVar> missingBounds;

-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);

-          if (missingBounds.Count != 0) {

-            e.MissingBounds = missingBounds;

-            if (e.Finite) {

-              foreach (var bv in e.MissingBounds) {

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

-              }

-            }

-          }

-        }

       } else if (expr is LambdaExpr) {

         var e = (LambdaExpr)expr;

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

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

         var e = (StmtExpr)expr;

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

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

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

         if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {

           var r = e.S as UpdateStmt;

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

@@ -10335,21 +10308,19 @@ namespace Microsoft.Dafny
         }

       } else if (expr is NamedExpr) {

         return moduleInfo.IsAbstract ? false : UsesSpecFeatures(((NamedExpr)expr).Body);

-      } else if (expr is ComprehensionExpr) {

-        var q = expr as QuantifierExpr;

-        Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution

-        if (q != null && q.Bounds.Contains(null)) {

-          return true;  // the quantifier cannot be compiled if the resolver found no bounds

-        }

-        return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));

+      } else if (expr is QuantifierExpr) {

+        var e = (QuantifierExpr)expr;

+        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

+        return e.UncompilableBoundVars().Count != 0;

       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

-        return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

+        return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

       } else if (expr is MapComprehension) {

         var e = (MapComprehension)expr;

-        return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));

+        return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || UsesSpecFeatures(e.Term);

       } else if (expr is LambdaExpr) {

-        return Contract.Exists(expr.SubExpressions, UsesSpecFeatures);

+        var e = (LambdaExpr)expr;

+        return UsesSpecFeatures(e.Term);

       } else if (expr is WildcardExpr) {

         return false;

       } else if (expr is StmtExpr) {

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 49e6efa0..e935c83d 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -586,16 +586,16 @@ method LetSuchThat(ghost z: int, n: nat)
 module NonInferredType {

   predicate P<T>(x: T)

 

-  method NonInferredType0(x: int)

+  method InferredType(x: int)

   {

     var t;

-    assume forall z :: P(z) && z == t;  // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.

+    assume forall z :: P(z) && z == t;

     assume t == x;  // this statement determines the type of t and z

   }

 

-  method NonInferredType1(x: int)

+  method NonInferredType(x: int)

   {

-    var t;

+    var t;  // error: the type of t is not determined

     assume forall z :: P(z) && z == t;  // error: the type of z is not determined

   }

 }

@@ -1126,15 +1126,15 @@ method TraitSynonym()
 // ----- set comprehensions where the term type is finite -----

 

 module ObjectSetComprehensions {

-  // allowed in non-ghost context:

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

+  // the following set comprehensions are known to be finite

+  function A() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

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

+  function method B() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

-  // not allowed in non-ghost context:

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

+  // outside functions, the comprehension is permitted, but it cannot be compiled

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

 

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

+  method D() { var x := set o : object | true :: o; }  // error: not (easily) compilable

 }

 

 // ------ regression test for type checking of integer division -----

@@ -1228,9 +1228,9 @@ module NonInferredTypeVariables {
   method BadClient(n: nat)

   {

     var p := P(n);  // error: cannot infer the type argument for P

-    ghost var q := Q(n);  // error: cannot infer the type argument for Q

+    ghost var q := Q(n);  // error: cannot infer the type argument for Q (and thus q's type cannot be determined either)

     M(n);  // error: cannot infer the type argument for M

-    var x := N(n);  // error: cannot infer the type argument for N

+    var x := N(n);  // error: cannot infer the type argument for N (and thus x's type cannot be determined either)

     var a := new array;  // error: cannot infer the type argument for 'array'

     var c := new C;  // error: cannot infer the type argument for 'C'

     var s: set;  // type argument for 'set' 

@@ -1248,7 +1248,7 @@ module NonInferredTypeVariables {
     ghost var d0 := forall s :: s == {7} ==> s != {};

     var d1 := forall s: set :: s in S ==> s == {};

     var ggcc0: C;

-    var ggcc1: C;

+    var ggcc1: C;  // error: full type cannot be determined

     ghost var d2 := forall c: C :: c != null ==> c.f == 10;

     ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;

     ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index edf61b33..be19eeac 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -20,10 +20,9 @@ ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree

-ResolutionErrors.dfy(592,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(592,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts

@@ -81,12 +80,28 @@ ResolutionErrors.dfy(1105,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P<int> and P<X>)

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

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

-ResolutionErrors.dfy(1135,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1130,31): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+ResolutionErrors.dfy(1132,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

 ResolutionErrors.dfy(1137,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined

+ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined

+ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined

+ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1254,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

+ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

@@ -209,4 +224,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-211 resolution/type errors detected in ResolutionErrors.dfy

+226 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy
index be092261..666d9575 100644
--- a/Test/dafny4/Regression0.dfy
+++ b/Test/dafny4/Regression0.dfy
@@ -4,10 +4,10 @@
 // This once crashed Dafny

 

 method M() {

-  var s := [1, "2"];

+  var s := [1, "2"];  // error: all elements must have the same type

   if * {

-    assert exists n :: n in s && n != 1;

+    assert exists n :: n in s && n != 1;  // the type of n is inferred to be int

   } else {

-    assert "2" in s;

+    assert "2" in s;  // error: since the type of s wasn't determined

   }

 }

diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect
index 9d1e3019..566b3e3f 100644
--- a/Test/dafny4/Regression0.dfy.expect
+++ b/Test/dafny4/Regression0.dfy.expect
@@ -1,4 +1,3 @@
 Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)

-Regression0.dfy(9,28): Error: the type of this variable is underspecified

 Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)

-3 resolution/type errors detected in Regression0.dfy

+2 resolution/type errors detected in Regression0.dfy

diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy
index 71a07f3d..d093a924 100644
--- a/Test/dafny4/set-compr.dfy
+++ b/Test/dafny4/set-compr.dfy
@@ -22,7 +22,7 @@ method O() returns (ghost p: set<object>)
 

 method P() returns (p: set<object>)

 {

-  p := set o: object | true;  // not allowed -- not in a ghost context

+  p := set o: object | true;  // error: not (easily) compilable

 }

 

 ghost method Q() returns (p: set<object>)

@@ -30,26 +30,54 @@ ghost method Q() returns (p: set<object>)
   p := set o: object | true;  // allowed, since the whole method is ghost

 }

 

-function F(): int

+function F(p: object): int

+  requires p in set o: object | true  // error: function is not allowed to depend on allocation state

+  ensures p in set o: object | true  // error: ditto (although one could argue that this would be okay)

+  reads set o: object | true  // error: same as for 'requires'

+  decreases set o: object | true  // error: same as for 'ensures'

+{

+  if p in set o: object | true then  // error: function is not allowed to depend on allocation state

+    F(p)

+  else

+    0

+}

+

+function method G(p: object): int

+  requires p in set o: object | true  // error (see F)

+  ensures p in set o: object | true  // error (see F)

+  reads set o: object | true  // error (see F)

+  decreases set o: object | true  // error (see F)

+{

+  if p in set o: object | true then  // error (see F)

+    G(p)

+  else

+    0

+}

+

+method M0() returns (ghost r: int, s: int)

   requires null in set o: object | true  // allowed

   ensures null in set o: object | true  // allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // allowed

 {

-  if null in set o: object | true then  // allowed -- in a ghost context

-    F()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

 

-function method G(): int

+method M1() returns (ghost r: int, s: int)

   requires null in set o: object | true  // (X) allowed

   ensures null in set o: object | true  // (X) allowed

-  reads set o: object | true  // allowed

+  modifies set o: object | true  // allowed

   decreases set o: object | true  // (X) allowed

 {

-  if null in set o: object | true then  // not allowed, since this is not a ghost context

-    G()

-  else

-    0

+  if null in set o: object | true {  // this makes the "if" a ghost

+    r := G(null);

+    s := G(null);  // error: assignment of non-ghost not allowed inside ghost "if"

+  } else {

+    r := 0;

+  }

 }

diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect
index 615ee2bc..b0490a11 100644
--- a/Test/dafny4/set-compr.dfy.expect
+++ b/Test/dafny4/set-compr.dfy.expect
@@ -1,3 +1,14 @@
 set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

-2 resolution/type errors detected in set-compr.dfy

+set-compr.dfy(34,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(35,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(36,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(37,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(39,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(46,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(47,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(48,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(49,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(51,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+set-compr.dfy(65,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+set-compr.dfy(79,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+13 resolution/type errors detected in set-compr.dfy

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index a6f8d922..60ac35f5 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -105,14 +105,14 @@ module WhatWeKnowAboutReads {
 
 module ReadsAll {
   function A(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o
+    reads set x,o | o in f.reads(x) :: o  // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
     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
+    reads set x,o | o in f.reads(x) :: o  // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
     requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)