diff options
| author |  qadeer <unknown> | 2013-11-22 11:19:15 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-11-22 11:19:15 -0800 |
| commit | f0d11b78f3453b5cfbb524e6d0c7214442814351 (patch) | |
| tree | 9dc4edc2cba5e3e1a0cce26194bf880b8679f57d /Test/test2 | |
| parent | 479fe0571200196552e3d415ab3b90e30083b1b2 (diff) | |
do monomorphic checking
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 29 |
1 files changed, 7 insertions, 22 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index e9390250..5c5fb9e0 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -482,12 +482,7 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
-------------------- Timeouts0.bpl --------------------
-Timeouts0.bpl(12,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(8,7): anon0
- Timeouts0.bpl(10,5): anon4_LoopHead
- Timeouts0.bpl(14,20): anon4_LoopBody
-Timeouts0.bpl(19,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(19,5): Error BP5003: A postcondition might not hold on this return path.
Timeouts0.bpl(4,3): Related location: This is the postcondition that might not hold.
Execution trace:
Timeouts0.bpl(8,7): anon0
@@ -495,19 +490,14 @@ Execution trace: Timeouts0.bpl(10,5): anon4_LoopDone
Timeouts0.bpl(19,5): anon5_LoopHead
Timeouts0.bpl(19,5): anon5_LoopDone
-Timeouts0.bpl(21,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Timeouts0.bpl(21,7): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Timeouts0.bpl(8,7): anon0
Timeouts0.bpl(10,5): anon4_LoopHead
Timeouts0.bpl(10,5): anon4_LoopDone
Timeouts0.bpl(19,5): anon5_LoopHead
Timeouts0.bpl(23,11): anon5_LoopBody
-Timeouts0.bpl(41,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(37,7): anon0
- Timeouts0.bpl(39,5): anon4_LoopHead
- Timeouts0.bpl(43,20): anon4_LoopBody
-Timeouts0.bpl(48,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
Execution trace:
Timeouts0.bpl(37,7): anon0
@@ -515,19 +505,14 @@ Execution trace: Timeouts0.bpl(39,5): anon4_LoopDone
Timeouts0.bpl(48,5): anon5_LoopHead
Timeouts0.bpl(48,5): anon5_LoopDone
-Timeouts0.bpl(50,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Timeouts0.bpl(50,7): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Timeouts0.bpl(37,7): anon0
Timeouts0.bpl(39,5): anon4_LoopHead
Timeouts0.bpl(39,5): anon4_LoopDone
Timeouts0.bpl(48,5): anon5_LoopHead
Timeouts0.bpl(52,11): anon5_LoopBody
-Timeouts0.bpl(70,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
-Execution trace:
- Timeouts0.bpl(66,7): anon0
- Timeouts0.bpl(68,5): anon4_LoopHead
- Timeouts0.bpl(72,20): anon4_LoopBody
-Timeouts0.bpl(77,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(77,5): Error BP5003: A postcondition might not hold on this return path.
Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
Execution trace:
Timeouts0.bpl(66,7): anon0
@@ -535,7 +520,7 @@ Execution trace: Timeouts0.bpl(68,5): anon4_LoopDone
Timeouts0.bpl(77,5): anon5_LoopHead
Timeouts0.bpl(77,5): anon5_LoopDone
-Timeouts0.bpl(79,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Timeouts0.bpl(79,7): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Timeouts0.bpl(66,7): anon0
Timeouts0.bpl(68,5): anon4_LoopHead
@@ -543,4 +528,4 @@ Execution trace: Timeouts0.bpl(77,5): anon5_LoopHead
Timeouts0.bpl(81,11): anon5_LoopBody
-Boogie program verifier finished with 0 verified, 0 errors, 3 time outs
+Boogie program verifier finished with 0 verified, 6 errors
|