(0,0): Error BP5001: This assertion might not hold. Execution trace: bar9.bpl(37,5): anon0 bar9.bpl(43,5): anon4_Else Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(20,7): anon2_Then Inlined call to procedure bar1 begins bar9.bpl(18,3): anon0 bar9.bpl(18,3): anon2_Else Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar1 ends Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(29,7): anon2_Then Inlined call to procedure bar2 begins bar9.bpl(28,3): anon0 bar9.bpl(28,3): anon2_Else Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends Inlined call to procedure bar2 ends bar9.bpl(46,3): anon3 Boogie program verifier finished with 0 verified, 1 error