4 files changed, 22 insertions, 18 deletions
diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 7e0ca1c4..6dedbada 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -58,7 +58,7 @@ function ok5(r : R):()
 // Reads checking where there are circularities among the expressions
 
 class CircularChecking {
-  var Repr: set<object>
+  ghost var Repr: set<object>
     
   function F(): int
     reads this, Repr
@@ -76,8 +76,8 @@ class CircularChecking {
     requires Repr == {}
 
   function H0(cell: Cell): int
-    reads Repr  // error: reads is not self-framing (unless "this in Repr")
-    requires this in Repr  // lo and behold!  So, reads clause is fine, if we can assume the precondition
+    reads Repr  // by itself, this reads is not self-framing
+    requires this in Repr  // lo and behold!  So, reads clause is fine after all
 
   function H1(cell: Cell): int
     reads this, Repr
@@ -126,3 +126,13 @@ function FunctionInQuantifier2(): int
   var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // fine :) :)
   f(10)
 }
+
+class DynamicFramesIdiom {
+  ghost var Repr: set<object>
+  predicate IllFormed_Valid()
+    reads Repr  // error: reads is not self framing (notice the absence of "this")
+  {
+    this in Repr  // this says that the predicate returns true if "this in Repr", but the
+                  // predicate can also be invoked in a state where its body will evaluate to false
+  }
+}
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 0b599f3f..1199797f 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,4 +1,4 @@
-Reads.dfy(79,11): Error: insufficient reads clause to read field
+Reads.dfy(133,11): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
 Reads.dfy(9,30): Error: insufficient reads clause to read field
@@ -7,8 +7,6 @@ Execution trace:
 Reads.dfy(18,30): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
-    (0,0): anon10_Then
-    (0,0): anon4
 Reads.dfy(28,50): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
@@ -32,4 +30,4 @@ Reads.dfy(120,38): Error: insufficient reads clause to invoke function
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 16 verified, 9 errors
+Dafny program verifier finished with 17 verified, 9 errors
diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy
index 2b892b35..0ceb46f1 100644
--- a/Test/hofs/Classes.dfy
+++ b/Test/hofs/Classes.dfy
@@ -30,15 +30,14 @@ function B(t : T) : int -> int
 }
 
 function J(t : T) : int
-  requires t != null;
-  requires t.h.reads(0) == {};
-  reads t;
-  reads if t != null then t.h.reads(0) else {};
+  requires t != null
+  reads t
+  reads t.h.reads(0)
 {
   if t.h.requires(0) then
     B(t)(0)
   else
-    B(t)(0)  // fail
+    B(t)(0)  // error: precondition violation
 }
 
 method U(t : T)
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect
index 21188d62..e490dbe0 100644
--- a/Test/hofs/Classes.dfy.expect
+++ b/Test/hofs/Classes.dfy.expect
@@ -1,10 +1,7 @@
-Classes.dfy(41,6): Error: possible violation of function precondition
+Classes.dfy(40,6): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
-    (0,0): anon13_Then
-    (0,0): anon4
-    (0,0): anon14_Then
-    (0,0): anon15_Else
-    (0,0): anon16_Else
+    (0,0): anon7_Else
+    (0,0): anon8_Else
 
 Dafny program verifier finished with 6 verified, 1 error