int h(int x, int y) {
  if (x != y) {
    if (2 * x == x + 10) {
      abort();
      /*error*/
    } else {
      return 2 x + y;
    }
  } else {
    return 2 x;
  }
}