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
|