diff options
Diffstat (limited to 'Test/extractloops')
| -rw-r--r-- | Test/extractloops/Answer | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index 9a6c95a3..954ea799 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -64,6 +64,10 @@ Boogie program verifier finished with 1 verified, 0 errors t3.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
t3.bpl(19,3): anon0
+ t3.bpl(23,3): anon3_LoopHead
+ Inlined call to procedure foo begins
+ t3.bpl(11,5): anon0
+ Inlined call to procedure foo ends
t3.bpl(27,3): anon3_LoopBody
t3.bpl(23,3): anon3_LoopHead
Inlined call to procedure foo begins
|