void main() {
  int x, y, NONDET;
  int old_x, old_y;

  while (x>0 && y > 0) {
    old_x = x;
    old_y = y;
    if ( NONDET ) {
      x = old_x-1;
      y = old_x;
    } else {
      x = old_y-2;
      y = old_x+1;
    }
  }

}