Do postponsed reads checking also for the body of functions -- see Test/dafny0/Reads.dfy for benefits.

(Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index f1c840c3..7e0ca1c4 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -123,6 +123,6 @@ function FunctionInQuantifier2(): int
   requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
   ensures FunctionInQuantifier2() == 100
 {
-  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // error: insufficient reads for f.reads(10)
+  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
   f(10)
 }