/*
 * A sample program for verification with CPAchecker.
 * Feb. 24, 2014, yoshiaki.takata@kochi-tech.ac.jp
 */
#define getInt __VERIFIER_nondet_getInt
extern int getInt(void);
extern int printInt(int);

void __assert(int prop) {
  if (! prop) {
    ERROR: goto ERROR;
  }
  return;
}

/*
 * Find the maximum value among three input integers.
 */
int main() {
  int a = getInt();
  int b = getInt();
  int c = getInt();
  int x;

  if (a > b) {
    if (b > c) { /* bug */
      x = a;
    } else {
      x = c;
    }
  } else {
    if (b > c) {
      x = b;
    } else {
      x = c;
    }
  }

  /* x is the maximum among a, b, and c. */
  __assert(x >= a && x >= b && x >= c && (x == a || x == b || x == c));

  printInt(x);
  return 0;
}