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
|
Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Elevator.bpl(18,3): anon0
Elevator.bpl(18,3): anon0$1
Elevator.bpl(19,3): anon10_LoopHead
Elevator.bpl(22,5): anon10_LoopBody
Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
Elevator.bpl(27,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
Elevator.bpl(20,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
Elevator.bpl(18,3): anon0
Elevator.bpl(71,23): inline$Initialize$0$Entry
Elevator.bpl(74,13): inline$Initialize$0$anon0
Elevator.bpl(71,23): inline$Initialize$0$Return
Elevator.bpl(18,3): anon0$1
Elevator.bpl(19,3): anon10_LoopHead
Elevator.bpl(22,5): anon10_LoopBody
Elevator.bpl(22,5): anon11_Else
Elevator.bpl(22,5): anon12_Else
Elevator.bpl(27,7): anon13_Then
Elevator.bpl(97,23): inline$MoveDown_Error$0$Entry
Elevator.bpl(102,3): inline$MoveDown_Error$0$anon0
Elevator.bpl(97,23): inline$MoveDown_Error$0$Return
Elevator.bpl(27,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
|
