blob: 02e7acb70ba5088b62a3a399c63d98ab5aa454ea (
plain)
1
2
3
4
5
6
7
8
|
Verification of basic.chalice using parameters=""
28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.
Boogie program verifier finished with 4 errors and 0 smoke test warnings.
|
