summaryrefslogtreecommitdiff
path: root/Test/inline/test5.bpl.expect
blob: cd0530dd876fc2965be07157e423862f2b53bcb1 (plain)
1
2
3
4
5
6
7
8
test5.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
    test5.bpl(36,10): anon0
    test5.bpl(30,10): inline$P$0$anon0
    test5.bpl(30,10): inline$P$1$anon0
    test5.bpl(36,10): anon0$2

Boogie program verifier finished with 4 verified, 1 error