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