diff options
Diffstat (limited to 'Test/dafny0/Reads.dfy')
| -rw-r--r-- | Test/dafny0/Reads.dfy | 2 |
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) } |