diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
| commit | e67c951ad9c5c637e36a6f025ba3d6e3ad945416 (patch) | |
| tree | 0cfb5c339602e4bdebf4bf97f3f0ccc3923c14d1 /Test/dafny0/CoinductiveProofs.dfy.expect | |
| parent | 000aa762e1fee4b9bd83ec3d7c8b61fd203e2c9d (diff) | |
| parent | df5c5f547990c1f80ab7594a1f9287ee03a61754 (diff) | |
Merge commit 'df5c5f5'
Diffstat (limited to 'Test/dafny0/CoinductiveProofs.dfy.expect')
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy.expect | 71 |
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
|