Using field access fails termination checking, while it succeeds with destructuring assignment

[utaal]

Given this definition:

struct Node<V> {
    v: V,
    next: Option<Box<Node<V>>>,
}

This works:

impl<V> Node<V> {
    #[ghost]
    fn len_logic(self: Node<V>) -> Int {
        {
            let Node { v: _, next } = self;
            1 + match next {
                Some(next) => next.len_logic(),
                None => 0,
            }
        }
    }
}

While this fails with "Cannot prove termination for len_logic":

impl<V> Node<V> {
    #[ghost]
    fn len_logic(self: Node<V>) -> Int {
        {
            1 + match self.next {
                Some(next) => next.len_logic(),
                None => 0,
            }
        }
    }
}

Note that the only difference is how next is accessed.