1 files changed, 23 insertions, 23 deletions
diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect
index 874df45e..7147ca60 100644
--- a/Test/dafny0/Datatypes.dfy.expect
+++ b/Test/dafny0/Datatypes.dfy.expect
@@ -1,43 +1,43 @@
-Datatypes.dfy(297,10): Error BP5003: A postcondition might not hold on this return path.
-Datatypes.dfy(295,15): Related location: This is the postcondition that might not hold.
+Datatypes.dfy(297,9): Error BP5003: A postcondition might not hold on this return path.
+Datatypes.dfy(295,14): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
     (0,0): anon13_Then
     (0,0): anon14_Else
     (0,0): anon15_Then
     (0,0): anon6
-Datatypes.dfy(298,12): Error: missing case in case statement: Appendix
+Datatypes.dfy(298,11): Error: missing case in case statement: Appendix
 Execution trace:
     (0,0): anon0
     (0,0): anon13_Then
     (0,0): anon14_Else
     (0,0): anon15_Else
     (0,0): anon16_Then
-Datatypes.dfy(349,5): Error: missing case in case statement: Cons
+Datatypes.dfy(349,4): Error: missing case in case statement: Cons
 Execution trace:
     (0,0): anon0
-    (0,0): anon6_Else
-    (0,0): anon7_Then
-Datatypes.dfy(349,5): Error: missing case in case statement: Nil
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Datatypes.dfy(349,4): Error: missing case in case statement: Nil
 Execution trace:
     (0,0): anon0
-    (0,0): anon6_Else
     (0,0): anon7_Else
-    (0,0): anon8_Then
-Datatypes.dfy(356,8): Error: missing case in case statement: Cons
+    (0,0): anon8_Else
+    (0,0): anon9_Then
+Datatypes.dfy(356,7): Error: missing case in case statement: Cons
 Execution trace:
     (0,0): anon0
-    (0,0): anon9_Else
-    (0,0): anon10_Then
+    (0,0): anon10_Else
     (0,0): anon11_Then
-Datatypes.dfy(356,8): Error: missing case in case statement: Nil
+    (0,0): anon12_Then
+Datatypes.dfy(356,7): Error: missing case in case statement: Nil
 Execution trace:
     (0,0): anon0
-    (0,0): anon9_Else
-    (0,0): anon10_Then
-    (0,0): anon11_Else
-    (0,0): anon12_Then
-Datatypes.dfy(82,20): Error: assertion violation
+    (0,0): anon10_Else
+    (0,0): anon11_Then
+    (0,0): anon12_Else
+    (0,0): anon13_Then
+Datatypes.dfy(82,19): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon20_Else
@@ -47,23 +47,23 @@ Execution trace:
     (0,0): anon23_Then
     (0,0): anon24_Else
     (0,0): anon25_Then
-Datatypes.dfy(170,16): Error: assertion violation
+Datatypes.dfy(170,15): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon4_Then
-Datatypes.dfy(172,16): Error: assertion violation
+Datatypes.dfy(172,15): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon4_Else
     (0,0): anon5_Then
-Datatypes.dfy(201,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Datatypes.dfy(201,12): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
 Execution trace:
     (0,0): anon0
-Datatypes.dfy(204,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Datatypes.dfy(204,16): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Then
-Datatypes.dfy(225,17): Error: destructor 'c' can only be applied to datatype values constructed by 'T''
+Datatypes.dfy(225,16): Error: destructor 'c' can only be applied to datatype values constructed by 'T''
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then