Verification of prog2.chalice using parameters="" 

  24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
  31.13: Location might not be readable.
  72.5: Const variable can be assigned to only once.
  77.5: Assertion might not hold. The expression at 77.12 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.
  20.3: The end of method Caller1 is unreachable.
  69.3: The end of method M2 is unreachable.

Boogie program verifier finished with 4 errors and 2 smoke test warnings.