Verification of prog1.chalice using parameters="" 

  9.10: Location might not be readable.
  25.5: Location might not be writable
  33.14: Location might not be readable.
  42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
  60.5: Location might not be writable
  76.5: The target of the unshare statement might not be shared.
  84.5: The target of the unshare statement might not be shared.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  7.3: The end of method seq0 is unreachable.
  21.3: The end of method seq3 is unreachable.
  28.3: The end of method main0 is unreachable.
  53.3: The end of method main3 is unreachable.
  73.3: The end of method main5 is unreachable.
  78.3: The end of method main6 is unreachable.

Boogie program verifier finished with 7 errors and 6 smoke test warnings.