CORE
main.c
--replace-call-with-contract ackermann
^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in main: SUCCESS$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
--
The Ackermann function has a function contract that the result
is always non-negative. This post-condition is necessary for establishing
the loop invariant. However, in this test, we do not enforce the function
contract. Instead, we assume that the function contract is correct and use it
(i.e. replace a recursive call of the Ackermann function with its contract).

We cannot verify/enforce the function contract of the Ackermann function, since
CBMC does not support function contracts for recursively defined functions.
As of now, CBMC only supports function contracts for non-recursive functions.