blob: 32b474f5a518d5e7b5f95629cb6e9afc6a575d04 (
plain)
1
2
3
4
5
6
7
|
chris5.bpl(15,3): Error BP5002: A precondition for this call might not hold.
chris5.bpl(6,3): Related location: This is the precondition that might not hold.
Execution trace:
chris5.bpl(13,3): anon0
(0,0): anon00
Boogie program verifier finished with 1 verified, 1 error
|
