Postpone reads checks of function preconditions until after the entire precondition has otherwise been checked for well-formedness

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 6ae07d53..545c9a18 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -72,7 +72,7 @@ class CircularChecking {
 
   function G1(): int
     reads this
-    requires F() == 100  // error: it is not known (yet) that the rest of what F() reads (namely, Repr) is empty
+    requires F() == 100  // fine, since the next line tells us that Repr is empty
     requires Repr == {}
 
   function H0(cell: Cell): int
@@ -86,7 +86,7 @@ class CircularChecking {
 
   function H2(cell: Cell): int
     reads this, Repr
-    requires cell != null && cell.data == 10  // error: it is not known (yet) that "cell in Repr"
+    requires cell != null && cell.data == 10  // this is okay, too, since reads checks are postponed
     requires cell in Repr
 }