Termination plugin incompleteness with let-expressions

[marcoeilers]

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.