Termination plugin incompleteness with let-expressions

For the following program, both backends report that len might not terminate:

field elem: Int
field nxt: Ref
predicate ll(r: Ref) {
    acc(r.elem) && acc(r.nxt) && (r.nxt != null ==> let rn == (r.nxt) in ll(rn))
}
function len(r: Ref): Int
    requires ll(r)
    decreases ll(r)
{
    unfolding ll(r) in (r.nxt == null ? 0 : 1 + len(r.nxt))
}

The program verifies if the let expression is removed and ll(rn) is replaced by ll(r.nxt).

Reported by @Aurel300, found by a PV student.

Start by running the provided program through both backends and compare it with the version where the let-expression is removed and ll(rn) uses ll(r.nxt). Trace the termination plugin's handling of let-expressions and identify why the decrease cannot be established. Done means both backends verify len without reporting possible nontermination.