diff options
Diffstat (limited to 'Test/dafny0/Answer')
-rw-r--r-- | Test/dafny0/Answer | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 97097cfd..36a6eda9 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1151,8 +1151,11 @@ Execution trace: Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon3_Else
+Corecursion.dfy(63,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
+Execution trace:
+ (0,0): anon5_Else
-Dafny program verifier finished with 5 verified, 2 errors
+Dafny program verifier finished with 7 verified, 3 errors
-------------------- CoResolution.dfy --------------------
CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default
@@ -1696,36 +1699,36 @@ Execution trace: Dafny program verifier finished with 1 verified, 4 errors
-------------------- Superposition.dfy --------------------
- +
Verifying CheckWellformed$$_0_M0.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_0_M0.C.M ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.P ...
[4 proof obligations] verified
- +
Verifying CheckWellformed$$_0_M0.C.Q ...
[3 proof obligations] error
Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_0_M0.C.R ...
[3 proof obligations] error
Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon5_Else
- +
Verifying CheckWellformed$$_1_M1.C.M ...
[0 proof obligations] verified
- +
Verifying Impl$$_1_M1.C.M ...
[1 proof obligation] verified
- +
Verifying CheckWellformed$$_1_M1.C.P ...
[1 proof obligation] error
Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.
@@ -1734,10 +1737,10 @@ Execution trace: (0,0): anon7_Else
(0,0): anon9_Then
(0,0): anon6
- +
Verifying CheckWellformed$$_1_M1.C.Q ...
[0 proof obligations] verified
- +
Verifying CheckWellformed$$_1_M1.C.R ...
[0 proof obligations] verified
|