2 files changed, 7 insertions, 11 deletions
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