----- Running regression test t1.bpl
t1.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
        t1.bpl(19,3): anon0
        t1.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t1.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t1.bpl(27,3): anon3_LoopBody
        t1.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t1.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t1.bpl(27,3): anon3_LoopBody
        t1.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t1.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t1.bpl(33,3): anon3_LoopDone
        t1.bpl(37,3): anon2

Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test t2.bpl
t2.bpl(51,5): Error BP5001: This assertion might not hold.
Execution trace:
        t2.bpl(19,3): anon0
        t2.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t2.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t2.bpl(27,3): anon3_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(37,3): lab1_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(37,3): lab1_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(42,3): lab1_LoopDone
        t2.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t2.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t2.bpl(27,3): anon3_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(37,3): lab1_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(37,3): lab1_LoopBody
        t2.bpl(34,3): lab1_LoopHead
        t2.bpl(42,3): lab1_LoopDone
        t2.bpl(23,3): anon3_LoopHead
        Inlined call to procedure foo begins
            t2.bpl(11,5): anon0
        Inlined call to procedure foo ends
        t2.bpl(46,3): anon3_LoopDone
        t2.bpl(50,3): anon2

Boogie program verifier finished with 0 verified, 1 error
-----