Mutually recursive calls not detected as infinite loop

[timotheeandres]

In our project, a function definition calls a lemma to prove that it is consistent. However, this lemma calls the function back to compute some result, but Stainless does not complain about it.

The call to the lemma is located here, in Ordinal.mult. This lemma calls the star operator of Ordinal, which itself calls Ordinal.mult.

When running Stainless with the command stainless --functions=mult,tailSmallerThanOmegaExp --solvers=smt-z3 implementation/* lemmas/*, all tests pass, even if the measure of the arguments a and b do not decrease between calls.