(0,0): Error BP5001: This assertion might not hold. Execution trace: bar10.bpl(37,5): anon0 Inlined call to procedure bar1 begins bar10.bpl(18,3): anon0 bar10.bpl(18,3): anon2_Else Inlined call to procedure bar1 ends Inlined call to procedure bar2 begins bar10.bpl(28,3): anon0 bar10.bpl(28,3): anon2_Else Inlined call to procedure bar2 ends Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar10.bpl(9,3): anon0 bar10.bpl(9,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