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

int main() {
    int x, y, z;
    x = 10; 
    y = -20;
    _(assert x < y)
    z = max(x,y);
}

int max(int a, int b)
_(requires a < b)
_(ensures \result >= a && \result >= b)
{
    if (a > b)
      return a;
    return b;
}

unsigned int addrec (unsigned int a, unsigned int b)
_(requires a + b < UINT_MAX)
_(ensures \result == a + b)
{
  if (b == 0)
    return a;
  else
    return (1 + addrec(a,b-1));
}