blob: 1e8d48898e4dbcc75fbb23f0a2e6f0bab745214c (
plain)
1
2
3
4
5
6
7
8
9
|
Assignment computed by Houdini:
b1 = False
b2 = True
houd2.bpl(14,1): Error BP5003: A postcondition might not hold on this return path.
houd2.bpl(11,1): Related location: This is the postcondition that might not hold.
Execution trace:
houd2.bpl(13,3): anon0
Boogie program verifier finished with 1 verified, 1 error
|
