#include <stdio.h>
#include <vcc.h>

_(requires \true)
_(ensures ((\result >= x) && (\result >= y) && (\result >= z))) 
{
  if (x <= y) {
    if (y <= z) {
      return z;
    }
    else {
      return y;
    }
  }
  else {
    if (x <= z) {
      return z;
    }
    else {
      return x;
    }
  }
}