----- Running regression test bar1.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar1.bpl(22,3): anon0 Inlined call to procedure foo begins bar1.bpl(13,5): anon0 Inlined call to procedure bar begins bar1.bpl(7,5): anon0 Inlined call to procedure bar ends Inlined call to procedure bar begins bar1.bpl(7,5): anon0 Inlined call to procedure bar ends Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar2.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar2.bpl(18,3): anon0 Inlined call to procedure foo begins bar2.bpl(4,3): anon0 bar2.bpl(5,7): anon3_Then Inlined call to procedure foo ends Inlined call to procedure foo begins bar2.bpl(4,3): anon0 bar2.bpl(8,7): anon3_Else Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar3.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar3.bpl(35,3): anon0 Inlined call to procedure foo begins bar3.bpl(18,3): anon0 bar3.bpl(19,7): anon3_Then Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(8,7): anon3_Then Inlined call to procedure bar ends Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(8,7): anon3_Then Inlined call to procedure bar ends Inlined call to procedure foo ends Inlined call to procedure bar begins bar3.bpl(7,3): anon0 bar3.bpl(10,7): anon3_Else Inlined call to procedure bar ends Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar4.bpl Boogie program verifier finished with 1 verified, 0 errors ----- ----- Running regression test bar6.bpl Boogie program verifier finished with 1 verified, 0 errors ----- ----- Running regression test bar7.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar7.bpl(35,5): anon0 bar7.bpl(37,5): anon4_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(7,3): anon0 bar7.bpl(7,3): anon2_Else Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends bar7.bpl(42,3): anon3 Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar8.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar8.bpl(34,5): anon0 bar8.bpl(36,5): anon4_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar8.bpl(7,3): anon0 bar8.bpl(7,3): anon2_Else Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends bar8.bpl(41,3): anon3 Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar9.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar9.bpl(35,5): anon0 bar9.bpl(41,5): anon4_Else Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(18,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(16,3): anon0 bar9.bpl(16,3): anon2_Else Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(27,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(26,3): anon0 bar9.bpl(26,3): anon2_Else Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends bar9.bpl(44,3): anon3 Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar10.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar10.bpl(35,5): anon0 Inlined call to procedure bar1 begins bar10.bpl(16,3): anon0 bar10.bpl(16,3): anon2_Else Inlined call to procedure bar1 ends Inlined call to procedure bar2 begins bar10.bpl(26,3): anon0 bar10.bpl(26,3): anon2_Else Inlined call to procedure bar2 ends Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(8,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(7,3): anon0 bar10.bpl(7,3): anon2_Else Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error ----- ----- Running regression test bar11.bpl (0,0): Error BP5001: This assertion might not hold. Execution trace: bar11.bpl(26,3): anon0 Inlined call to procedure foo begins bar11.bpl(15,3): anon0 value = 0 Inlined call to procedure bar begins bar11.bpl(8,5): anon0 value = 1 Inlined call to procedure bar ends Inlined call to procedure bar begins bar11.bpl(8,5): anon0 value = 2 Inlined call to procedure bar ends value = 2 Inlined call to procedure foo ends Boogie program verifier finished with 0 verified, 1 error -----