Verification of locks.chalice 

  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.

Boogie program verifier finished with 20 verified, 10 errors