Verification of sequences.chalice 

  36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
  60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f

Boogie program verifier finished with 20 verified, 2 errors