1 files changed, 13 insertions, 13 deletions
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
index 98aa0cd8..69cb360d 100644
--- a/Test/dafny0/Termination.dfy.expect
+++ b/Test/dafny0/Termination.dfy.expect
@@ -1,20 +1,20 @@
-Termination.dfy[TerminationRefinement1](441,6): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](441,5): Error: failure to decrease termination measure
 Execution trace:
     (0,0): anon0
-Termination.dfy(361,47): Error: failure to decrease termination measure
+Termination.dfy(361,46): Error: failure to decrease termination measure
 Execution trace:
     (0,0): anon0
-    (0,0): anon7_Else
-    (0,0): anon8_Then
     (0,0): anon9_Else
-Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+    (0,0): anon10_Then
+    (0,0): anon11_Else
+Termination.dfy(108,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Execution trace:
     (0,0): anon0
     Termination.dfy(108,3): anon6_LoopHead
     (0,0): anon6_LoopBody
     Termination.dfy(108,3): anon7_Else
     Termination.dfy(108,3): anon8_Else
-Termination.dfy(116,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(116,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Execution trace:
     (0,0): anon0
     Termination.dfy(116,3): anon8_LoopHead
@@ -23,7 +23,7 @@ Execution trace:
     (0,0): anon10_Then
     (0,0): anon5
     Termination.dfy(116,3): anon11_Else
-Termination.dfy(125,3): Error: decreases expression might not decrease
+Termination.dfy(125,2): Error: decreases expression might not decrease
 Execution trace:
     (0,0): anon0
     Termination.dfy(125,3): anon8_LoopHead
@@ -32,7 +32,7 @@ Execution trace:
     (0,0): anon10_Then
     (0,0): anon5
     Termination.dfy(125,3): anon11_Else
-Termination.dfy(126,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(126,16): Error: decreases expression must be bounded below by 0 at end of loop iteration
 Execution trace:
     (0,0): anon0
     Termination.dfy(125,3): anon8_LoopHead
@@ -41,13 +41,13 @@ Execution trace:
     (0,0): anon10_Then
     (0,0): anon5
     Termination.dfy(125,3): anon11_Else
-Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause
 Execution trace:
     (0,0): anon0
-    (0,0): anon6_Else
-    (0,0): anon7_Else
-    (0,0): anon8_Then
-Termination.dfy(296,3): Error: decreases expression might not decrease
+    (0,0): anon8_Else
+    (0,0): anon9_Else
+    (0,0): anon10_Then
+Termination.dfy(296,2): Error: decreases expression might not decrease
 Execution trace:
     Termination.dfy(296,3): anon9_LoopHead
     (0,0): anon9_LoopBody