blob: 9780a21f79f598bb7a62741116d31d13d53d80a2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
t1.bpl(19,3): anon0
t1.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t1.bpl(10,5): anon0
Inlined call to procedure foo ends
t1.bpl(28,3): anon3_LoopBody
t1.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t1.bpl(10,5): anon0
Inlined call to procedure foo ends
t1.bpl(28,3): anon3_LoopBody
t1.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t1.bpl(10,5): anon0
Inlined call to procedure foo ends
t1.bpl(34,3): anon3_LoopDone
t1.bpl(38,3): anon2
Boogie program verifier finished with 0 verified, 1 error
|
