summaryrefslogtreecommitdiff
path: root/Test/linear/f2.bpl.expect
blob: a28b70381657dd0776f89f7b620dc440009a747a (plain)
1
2
3
4
5
f2.bpl(21,4): Error BP5001: This assertion might not hold.
Execution trace:
    f2.bpl(17,4): anon0

Boogie program verifier finished with 0 verified, 1 error