1 files changed, 30 insertions, 0 deletions
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index 47f7f575..d0a8b43b 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -101,3 +101,33 @@ module WhatWeKnowAboutReads {
     }
   }
 }
+
+module ReadsAll {
+  function A(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    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;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function C(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method D(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+}