Failure when extracting a loop with a shared borrow

[RaitoBezarius]

RaitoBezarius/avl-verification@117cd1c fails extraction with Aeneas:

❯ nix run github:aeneasverif/aeneas -L -- -backend lean avl_verification.llbc
[Info ] Imported: avl_verification.llbc
[Info ] Generated the partial file (because of errors): ./AvlVerification.lean
[Error] There should be no bottoms in the value
Source: 'src/main.rs', lines 33:52-39:9

related to the find function.

[sonmarcho]

Slightly minimized example:

struct AVLNode {
    child: Option<Box<AVLNode>>,
}

struct AVLTreeSet {
    root: Option<Box<AVLNode>>,
}

impl AVLNode {
    pub fn find(self) -> bool {
        let mut current_tree = &self.child; // This is the root of the problem in the computation of the fixed point

        while let Some(current_node) = current_tree {
            current_tree = &current_node.child;
        }

        false
    }
}