#include <vcc.h>
#include <limits.h>

void main() {
  int a;
  a = fun(0);
  _(assert(a == 0))
}

int fun (int x)
_(requires \true) 
_(ensures \result >= x) {
  return x;
}