Verification of basic.chalice using parameters="" 

  28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
  48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
  97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
  148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.

Boogie program verifier finished with 41 verified, 4 errors