blob: a00bd2184e2122710156609d4e74d2d00be20dd2 (
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:
bar3.bpl(37,3): anon0
Inlined call to procedure foo begins
bar3.bpl(20,3): anon0
bar3.bpl(21,7): anon3_Then
Inlined call to procedure bar begins
bar3.bpl(9,3): anon0
bar3.bpl(10,7): anon3_Then
Inlined call to procedure bar ends
Inlined call to procedure bar begins
bar3.bpl(9,3): anon0
bar3.bpl(10,7): anon3_Then
Inlined call to procedure bar ends
Inlined call to procedure foo ends
Inlined call to procedure bar begins
bar3.bpl(9,3): anon0
bar3.bpl(12,7): anon3_Else
Inlined call to procedure bar ends
Boogie program verifier finished with 0 verified, 1 error
|
