Auto-merged heads.

6 files changed, 27 insertions, 31 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 3c933bae..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): anon11_Then

-    (0,0): anon3

-    (0,0): anon12_Then

-    (0,0): anon13_Else

-    (0,0): anon14_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Else

 

 Dafny program verifier finished with 6 verified, 1 error

diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index 62c035b2..b4dfc561 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -1,20 +1,20 @@
 Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Else

-    (0,0): anon9_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Else

+    (0,0): anon11_Then

 Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon8_Else

     (0,0): anon9_Else

+    (0,0): anon10_Else

+    (0,0): anon11_Else

 Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Else

 Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

@@ -24,12 +24,12 @@ Execution trace:
 Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Naked.dfy(29,30): Error: possible violation of function precondition

 Naked.dfy(32,14): Related location

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

@@ -42,7 +42,7 @@ Execution trace:
 Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index 73002b73..cd013630 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -1,19 +1,19 @@
 ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Else

+    (0,0): anon4_Else

 ReadsReads.dfy(87,50): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index b3c126d5..1a1027ae 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -1,13 +1,13 @@
 Simple.dfy(14,10): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

 Simple.dfy(27,10): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-    (0,0): anon6_Then

+    (0,0): anon6_Else

+    (0,0): anon7_Then

 Simple.dfy(37,9): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect
index 5ba4b47b..2476b945 100644
--- a/Test/hofs/Twice.dfy.expect
+++ b/Test/hofs/Twice.dfy.expect
@@ -5,7 +5,7 @@ Execution trace:
 Twice.dfy(35,32): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Else

-    (0,0): anon10_Then

+    (0,0): anon10_Else

+    (0,0): anon11_Then

 

 Dafny program verifier finished with 4 verified, 2 errors