blob: 80eeb1a7ec378d16bfae72e4187636dca7b61036 (
plain)
1
2
3
4
5
6
7
8
|
Bug25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
Bug25.bpl(8,1): Related location: This is the postcondition that might not hold.
Execution trace:
Bug25.bpl(11,3): anon0
Bug25.bpl(12,1): anon2_LoopHead
Bug25.bpl(12,1): anon2_LoopDone
Boogie program verifier finished with 0 verified, 1 error
|
