procedure M (i: int) {
  assert i != 0;
}