1 files changed, 18 insertions, 18 deletions
diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect
index e30f6f1a..a6b3fdce 100644
--- a/Test/dafny0/Corecursion.dfy.expect
+++ b/Test/dafny0/Corecursion.dfy.expect
@@ -1,36 +1,36 @@
-Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
+Corecursion.dfy(17,12): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
 Execution trace:
     (0,0): anon0
-    (0,0): anon3_Else
-Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
+    (0,0): anon4_Else
+Corecursion.dfy(23,12): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
 Execution trace:
     (0,0): anon0
-    (0,0): anon3_Else
-Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause
+    (0,0): anon4_Else
+Corecursion.dfy(58,4): Error: cannot prove termination; try supplying a decreases clause
 Execution trace:
     (0,0): anon0
-    (0,0): anon3_Else
-Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
+    (0,0): anon4_Else
+Corecursion.dfy(71,15): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
 Execution trace:
     (0,0): anon0
-    (0,0): anon5_Else
-Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+    (0,0): anon7_Else
+Corecursion.dfy(93,14): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
 Execution trace:
     (0,0): anon0
-    (0,0): anon5_Else
-    (0,0): anon6_Then
-Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Corecursion.dfy(103,14): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
 Execution trace:
     (0,0): anon0
-    (0,0): anon5_Else
-    (0,0): anon6_Then
-Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Corecursion.dfy(148,12): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
 Execution trace:
     (0,0): anon0
-    (0,0): anon3_Else
-Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
+    (0,0): anon4_Else
+Corecursion.dfy(161,12): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)
 Execution trace:
     (0,0): anon0
-    (0,0): anon3_Else
+    (0,0): anon4_Else
 
 Dafny program verifier finished with 20 verified, 8 errors