blob: b2bf49bdb7822bf2ad77ef08e1ec185c2441b0f0 (
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
|
