1 files changed, 49 insertions, 22 deletions
diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect
index 12ce2f01..c4f4c405 100644
--- a/Test/dafny0/CoinductiveProofs.dfy.expect
+++ b/Test/dafny0/CoinductiveProofs.dfy.expect
@@ -1,50 +1,77 @@
-CoinductiveProofs.dfy(29,12): Error: assertion violation
-CoinductiveProofs.dfy(13,17): Related location
+CoinductiveProofs.dfy(30,11): Error: assertion violation
+CoinductiveProofs.dfy(15,36): Related location
+CoinductiveProofs.dfy(13,16): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
     (0,0): anon6_Then
-CoinductiveProofs.dfy(59,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(58,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(54,3): Related location
+CoinductiveProofs.dfy(44,11): Error: assertion violation
+CoinductiveProofs.dfy(13,16): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon13_Then
+    (0,0): anon16_Then
+CoinductiveProofs.dfy(48,11): Error: assertion violation
+CoinductiveProofs.dfy(13,16): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon13_Then
+    (0,0): anon18_Then
+CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(73,2): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
-CoinductiveProofs.dfy(74,12): Error: assertion violation
-CoinductiveProofs.dfy(54,3): Related location
+CoinductiveProofs.dfy(94,11): Error: assertion violation
+CoinductiveProofs.dfy(87,29): Related location
+CoinductiveProofs.dfy(73,2): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
     (0,0): anon6_Then
-CoinductiveProofs.dfy(91,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(90,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(80,3): Related location
+CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(115,2): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
-CoinductiveProofs.dfy(100,12): Error: assertion violation
-CoinductiveProofs.dfy(80,3): Related location
+CoinductiveProofs.dfy(136,11): Error: assertion violation
+CoinductiveProofs.dfy(117,29): Related location
+CoinductiveProofs.dfy(115,2): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
     (0,0): anon6_Then
-CoinductiveProofs.dfy(111,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(110,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(106,3): Related location
+CoinductiveProofs.dfy(149,11): Error: assertion violation
+CoinductiveProofs.dfy(115,2): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon13_Then
+    (0,0): anon16_Then
+CoinductiveProofs.dfy(153,11): Error: assertion violation
+CoinductiveProofs.dfy(115,2): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon13_Then
+    (0,0): anon18_Then
+CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(159,2): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
-CoinductiveProofs.dfy(150,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(149,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(4,24): Related location
+CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(4,23): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
-CoinductiveProofs.dfy(156,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(155,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(4,24): Related location
+CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(4,23): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon3_Then
 
-Dafny program verifier finished with 35 verified, 8 errors
+Dafny program verifier finished with 42 verified, 12 errors