Verification of permission_arithmetic.chalice using parameters="" 

  26.5: Assertion might not hold. The permission at 26.12 might not be positive.
  42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive.
  75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x.
  88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22  for Cell.x.
  105.20: Location might not be readable.
  111.20: Location might not be readable.
  147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x.
  164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive.
  176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x.
  205.10: Location might not be readable.
  220.10: 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.
  18.3: Precondition of method a2 is equivalent to false.
  24.3: The end of method a3 is unreachable.
  42.5: The statements after the method call statement are unreachable.
  200.3: The end of method a28 is unreachable.
  215.3: The end of method a28b is unreachable.

Boogie program verifier finished with 11 errors and 5 smoke test warnings.