path: root/Test/test15/IntInModel.bpl

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