Verification of test7.chalice using parameters="" 

  31.5: The precondition at 14.14 might not hold. Insufficient fraction at 14.14 for C.inv.
  67.5: Assertion might not hold. Insufficient fraction at 67.12 for C.value.
  91.5: Assertion might not hold. Insufficient fraction at 91.12 for C.inv.
  95.14: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv.
  99.14: Location might not be readable.
  103.28: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv.
  107.21: Location might not be readable.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  31.5: The statements after the method call statement are unreachable.
  62.3: The end of method uf0 is unreachable.
  86.3: The end of method uf3 is unreachable.

Boogie program verifier finished with 7 errors and 3 smoke test warnings.