diff options
Diffstat (limited to 'Test/inline/Elevator.bpl.expect')
| -rw-r--r-- | Test/inline/Elevator.bpl.expect | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Test/inline/Elevator.bpl.expect b/Test/inline/Elevator.bpl.expect new file mode 100644 index 00000000..87141605 --- /dev/null +++ b/Test/inline/Elevator.bpl.expect @@ -0,0 +1,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 |