/*
 * A sample program for verification with CPAchecker.
 * Although this program is safe, CPAchecker answers that it is unsafe.
 * 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[3];
  int x, i;
  a[0] = getInt();
  a[1] = getInt();
  a[2] = getInt();

  x = a[0];
  i = 1;
  if (x < a[i]) {
    x = a[i];
  }
  i = 2;
  if (x < a[i]) {
    x = a[i];
  }

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

  printInt(x);
  return 0;
}