Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

1 files changed, 2 insertions, 2 deletions

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)