Fails to prove termination when recursive calls are placed inside a loop

[rikosellic]

The following function fails to prove termination unless annotated with #[verifier::loop_isolation(false)]:

pub fn test(x: usize)
    decreases x,
{
    if x == 0 {
        return;
    }
    for i in 0..1 {
        test(x - 1);
    }
}

Is this a reasonable default behavior? It seems the user can not express explicit termination-related conditions in the loop invariant, so loop_isolation(false) is the only solution.

[tjhance]

this does seem to be a verus bug. (for anyone else wondering, the issue doesn't seem to have to do with the underflow error. i.e., if you add invariant x >= 1 then verus still fails to prove termination.)