Open RaitoBezarius opened 7 months ago
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 = ¤t_node.child;
}
false
}
}
https://github.com/RaitoBezarius/avl-verification/commit/117cd1c0afbc50ffc5a90473cb4c01185188711e fails extraction with Aeneas:
related to the
find
function.