blob: 2cb8d25db7f377415895443e5418c8434d11cd2e (
plain)
1
2
3
4
5
6
7
|
Verification of sequences.chalice using parameters=""
36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
Boogie program verifier finished with 2 errors and 0 smoke test warnings.
|
