Verification of locks.chalice using parameters="" 

  21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
  24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
  44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x.
  54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x.
  73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x.
  80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x.
  83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x.
  103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x.
  111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x.
  136.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.
  66.3: The end of method a1 is unreachable.
  76.3: The end of method a2 is unreachable.
  86.3: The end of method a3 is unreachable.
  138.5: The statements after the acquire statement are unreachable.

Boogie program verifier finished with 10 errors and 4 smoke test warnings.