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

unsigned add(unsigned n, unsigned m)
_(requires m + n <= UINT_MAX)
_(ensures \result == n + m) {
  unsigned  a = m;
  unsigned  x = 0;
  while (x < n) 
  _(invariant (a == n + x) && (x <= n)) {
    a = a + 1;
    x = x + 1;
  }
  return a;
}