Verification of workitem-10195.chalice using parameters="" 

  4.14: Range minimum might not be smaller or equal to range maximum.
  10.14: Range minimum might not be smaller or equal to range maximum.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  2.5: The end of method fails is unreachable.
  8.5: The end of method succeeds1 is unreachable.
  19.9: Precondition of method succeeds2 is equivalent to false.
  27.9: Precondition of method fails2 is equivalent to false.

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