blob: bd34d3802fb683386e7560826ce6dbeb9af889d5 (
plain)
1
2
3
4
5
6
|
Verification of UnboundedThreads.chalice using parameters=""
40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27 for C.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 1 errors and 0 smoke test warnings.
|
