Check the when-condition for recursive call of spec fn

[WeituoDAI]

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Related to #2036 .

I notice that the decrease_when condition is not checked when it is recursively called inside a spec fn. For example, the definition below is allowed currently.

spec fn h(x:int) -> int
    decreases x when x > 1
{
    h(x-1)
}

And an example found in examples/syntax.rs :

spec fn dec0(a: int) -> int
    decreases a,
    when a > 0
    via dec0_decreases
{
    if a > 0 {
        dec0(a - 1)
    } else {
        0
    }
}

In fact, we cannot do any meaningful proof about this dec0, since any call of dec0(a) (a>0) will recursively call dec0(0) at last, but it is uninterp since it does not meet the when-condition (If I make no mistake, the decrease_when is implemented as such).

It does not lead to soundness problem, but it must be a bug. For any recursive function f, We know f(x) is uninterp if x does not meet the when-condition; if inside its body, there is a recursive call f(y) where y does not meet the when-condition, then the function can only return uninterp..

In my eyes, decrease_when should really work like a pre-condition here.

So I (1) add the check of when-condition for any recursive call inside the body of spec function (2) change some related testcase