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