1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
Where.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(8,3): anon0
Where.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(18,5): anon0
Where.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(32,3): anon0
Where.bpl(46,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(42,5): anon0
Where.bpl(59,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(54,3): anon0
Where.bpl(113,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(104,5): anon0
Where.bpl(106,3): anon3_LoopHead
Where.bpl(106,3): anon3_LoopDone
Where.bpl(130,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(123,5): anon0
Where.bpl(124,3): anon3_LoopHead
Where.bpl(124,3): anon3_LoopDone
Where.bpl(147,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(140,5): anon0
Where.bpl(141,3): anon3_LoopHead
Where.bpl(141,3): anon3_LoopDone
Where.bpl(164,3): Error BP5001: This assertion might not hold.
Execution trace:
Where.bpl(157,5): anon0
Where.bpl(158,3): anon3_LoopHead
Where.bpl(158,3): anon3_LoopDone
Boogie program verifier finished with 2 verified, 9 errors
|
