(0,0): Error BP5001: This assertion might not hold. Execution trace: bar7.bpl(37,5): anon0 bar7.bpl(39,5): anon4_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.bpl(10,9): anon2_Then Inlined call to procedure foo begins bar7.bpl(9,3): anon0 bar7.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 bar7.bpl(44,3): anon3 Boogie program verifier finished with 0 verified, 1 error