/* 
  an example from llreve:
  http://formal.iti.kit.edu/projects/improve/reve/
*/

int f1(int n) {
  int r;
  int rx;
  int nx;

  r = 0;
  rx = 0;
  nx = 0;

  if (n <= 1) {
    r = n;
  } else {
    // BEGIN INLINING
    nx = n - 1;
    rx = 0;
    if (nx <= 1) {
      rx = nx;
    } else {
      rx = f1(nx - 1);
      rx = nx + rx;
    }
    r = rx;
    // END INLINING
    r = n + r;
  }

  return r;
}

int f2(int n) {
  int r;
  r = 0;

  if (n <= 1) {
    r = n;
  } else {
    r = f2(n - 2);
    r = n + (n-1) + r;
  }

  return r;
}
