Verification of prog4.chalice using parameters="" 

  5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
  17.7: The target of the release statement might not be locked by the current thread.
  17.7: Release might fail because the current thread might hold the read lock.
  30.7: The target of the release statement might not be locked by the current thread.
  30.7: Release might fail because the current thread might hold the read lock.
  34.5: The target of the release statement might not be locked by the current thread.
  34.5: Release might fail because the current thread might hold the read lock.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  2.3: The end of method M is unreachable.

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