/*@
// The McCarthy 91 function
logic integer McCarthy91(integer n) =
(n > 100) ? n - 10 : McCarthy91(McCarthy91(n + 11));

// Iterated application of McCarthy91, k times
logic integer McCarthy_iter(integer n, integer k) =
(k == 0) ? n : McCarthy91(McCarthy_iter(n, k - 1));
*/

/*@
requires \true;
ensures \result == McCarthy91(\old(n));
*/
int mccarthy_91_non_recursive(int n) {
//@ ghost int n0 = n;
int c = 1;

/*@
loop invariant c >= 0;
loop invariant n == McCarthy_iter(n0, c);
loop assigns n, c;
loop variant c;
*/
while (c != 0) {
if (n > 100) {
n = n - 10;
c--;
} else {
n = n + 11;
c++;
}
}

return n;
}