blob: 2f4acf7b97b33a063190a027243e66aa0b8959f0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Verification of predicates.chalice using parameters=""
37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.
55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.
66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
28.3: The end of method b3 is unreachable.
49.3: The end of method b5 is unreachable.
Boogie program verifier finished with 3 errors and 2 smoke test warnings
|
