Verification of SmokeTestTest.chalice using parameters="" 

  106.3: The postcondition at 107.13 might not hold. The expression at 107.13 might not evaluate to true.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  2.1: Monitor invariant is equivalent to false.
  8.3: Precondition of method a1 is equivalent to false.
  12.3: Precondition of method a2 is equivalent to false.
  27.5: The begging of the if-branch is unreachable.
  43.5: The begging of the if-branch is unreachable.
  53.5: Assumption introduces a contradiction.
  59.5: The statements after the while-loop are unreachable.
  76.5: The begging of the else-branch is unreachable.
  83.3: Precondition of function f1 is equivalent to false.
  90.5: The begging of the if-branch is unreachable.
  93.7: The begging of the else-branch is unreachable.
  93.19: Assumption introduces a contradiction.
  100.5: Assumption introduces a contradiction.
  113.5: The statements after the method call statement are unreachable.
  116.3: Predicate Cell.valid is equivalent to false.
  121.1: Where clause of channel C is equivalent to false.

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