blob: cdcdd0f24106077b1309716e199fc6fff1361dfc (
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:
t3.bpl(19,3): anon0
t3.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t3.bpl(10,5): anon0
Inlined call to procedure foo ends
t3.bpl(28,3): anon3_LoopBody
t3.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t3.bpl(10,5): anon0
Inlined call to procedure foo ends
t3.bpl(28,3): anon3_LoopBody
t3.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t3.bpl(10,5): anon0
Inlined call to procedure foo ends
t3.bpl(34,3): anon3_LoopDone
t3.bpl(38,3): anon2
Boogie program verifier finished with 0 verified, 1 error
|
