(0,0): Error BP5001: This assertion might not hold.
Execution trace:
    bar1.bpl(24,3): anon0
    Inlined call to procedure foo begins
        bar1.bpl(15,5): anon0
        Inlined call to procedure bar begins
            bar1.bpl(9,5): anon0
        Inlined call to procedure bar ends
        Inlined call to procedure bar begins
            bar1.bpl(9,5): anon0
        Inlined call to procedure bar ends
    Inlined call to procedure foo ends

Boogie program verifier finished with 0 verified, 1 error