blob: bd5dbbf43e513b8b9125120f8f9b66099246df64 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar11.bpl(28,3): anon0
Inlined call to procedure foo begins
bar11.bpl(17,3): anon0
value = 0
Inlined call to procedure bar begins
bar11.bpl(10,5): anon0
value = 1
Inlined call to procedure bar ends
Inlined call to procedure bar begins
bar11.bpl(10,5): anon0
value = 2
Inlined call to procedure bar ends
value = 2
Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
|
