(0,0): Error BP5001: This assertion might not hold.
Execution trace:
    bar11.bpl(28,3): anon0
    Inlined call to procedure foo begins
        bar11.bpl(17,3): anon0
        value = 0
        Inlined call to procedure bar begins
            bar11.bpl(10,5): anon0
            value = 1
        Inlined call to procedure bar ends
        Inlined call to procedure bar begins
            bar11.bpl(10,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