diff --git a/tests/lean/NaiveTree/Funs.lean b/tests/lean/NaiveTree/Funs.lean
new file mode 100644
index 000000000..88703c18c
--- /dev/null
+++ b/tests/lean/NaiveTree/Funs.lean
@@ -0,0 +1,76 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [naive_tree]: function definitions
+import Base
+import NaiveTree.Types
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace naive_tree
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::new]:
+   Source: 'src/naive-tree.rs', lines 34:4-34:24 -/
+def TreeSet.new (T : Type) (OrdInst : Ord T) : Result (TreeSet T) :=
+  Result.ok { root := none }
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::find]: loop 0:
+   Source: 'src/naive-tree.rs', lines 38:4-50:5 -/
+divergent def TreeSet.find_loop
+  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
+  Result Bool
+  :=
+  match current_tree with
+  | none => Result.ok false
+  | some current_node =>
+    do
+    let o ← OrdInst.cmp current_node.value value
+    match o with
+    | Ordering.Less => TreeSet.find_loop T OrdInst value current_node.right
+    | Ordering.Equal => Result.ok true
+    | Ordering.Greater => TreeSet.find_loop T OrdInst value current_node.left
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::find]:
+   Source: 'src/naive-tree.rs', lines 38:4-38:40 -/
+def TreeSet.find
+  (T : Type) (OrdInst : Ord T) (self : TreeSet T) (value : T) : Result Bool :=
+  TreeSet.find_loop T OrdInst value self.root
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::insert]: loop 0:
+   Source: 'src/naive-tree.rs', lines 51:4-69:5 -/
+divergent def TreeSet.insert_loop
+  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
+  Result (Bool × (Option (Node T)))
+  :=
+  match current_tree with
+  | none => let n := Node.mk value none none
+            Result.ok (true, some n)
+  | some current_node =>
+    do
+    let o ← OrdInst.cmp current_node.value value
+    match o with
+    | Ordering.Less =>
+      do
+      let (b, current_tree1) ←
+        TreeSet.insert_loop T OrdInst value current_node.right
+      Result.ok (b, some (Node.mk current_node.value current_node.left
+        current_tree1))
+    | Ordering.Equal => Result.ok (false, some current_node)
+    | Ordering.Greater =>
+      do
+      let (b, current_tree1) ←
+        TreeSet.insert_loop T OrdInst value current_node.left
+      Result.ok (b, some (Node.mk current_node.value current_tree1
+        current_node.right))
+
+/- [naive_tree::{naive_tree::TreeSet<T>}::insert]:
+   Source: 'src/naive-tree.rs', lines 51:4-51:46 -/
+def TreeSet.insert
+  (T : Type) (OrdInst : Ord T) (self : TreeSet T) (value : T) :
+  Result (Bool × (TreeSet T))
+  :=
+  do
+  let (b, ts) ← TreeSet.insert_loop T OrdInst value self.root
+  Result.ok (b, { root := ts })
+
+end naive_tree
diff --git a/tests/lean/NaiveTree/Types.lean b/tests/lean/NaiveTree/Types.lean
new file mode 100644
index 000000000..0d53847b7
--- /dev/null
+++ b/tests/lean/NaiveTree/Types.lean
@@ -0,0 +1,66 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [naive_tree]: type definitions
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace naive_tree
+
+/- [naive_tree::Ordering]
+   Source: 'src/naive-tree.rs', lines 5:0-5:17 -/
+inductive Ordering :=
+| Less : Ordering
+| Equal : Ordering
+| Greater : Ordering
+
+/- Trait declaration: [naive_tree::Ord]
+   Source: 'src/naive-tree.rs', lines 11:0-11:9 -/
+structure Ord (Self : Type) where
+  cmp : Self → Self → Result Ordering
+
+/- Trait declaration: [naive_tree::Bounded]
+   Source: 'src/naive-tree.rs', lines 15:0-15:13 -/
+structure Bounded (Self : Type) where
+  Value : Type
+  max_value : Result Value
+  min_value : Result Value
+
+/- [naive_tree::Node]
+   Source: 'src/naive-tree.rs', lines 21:0-21:14 -/
+inductive Node (T : Type) :=
+| mk : T → Option (Node T) → Option (Node T) → Node T
+
+@[reducible]
+def Node.value {T : Type} (x : Node T) :=
+  match x with | Node.mk x1 _ _ => x1
+
+@[reducible]
+def Node.left {T : Type} (x : Node T) :=
+  match x with | Node.mk _ x1 _ => x1
+
+@[reducible]
+def Node.right {T : Type} (x : Node T) :=
+  match x with | Node.mk _ _ x1 => x1
+
+@[simp]
+theorem Node.value._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).value = value :=
+  by rfl
+
+@[simp]
+theorem Node.left._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).left = left := by rfl
+
+@[simp]
+theorem Node.right._simpLemma_ {T : Type} (value : T) (left : Option (Node T))
+  (right : Option (Node T)) : (Node.mk value left right).right = right :=
+  by rfl
+
+/- [naive_tree::TreeSet]
+   Source: 'src/naive-tree.rs', lines 29:0-29:17 -/
+structure TreeSet (T : Type) where
+  root : Option (Node T)
+
+end naive_tree
diff --git a/tests/src/naive-tree/Cargo.lock b/tests/src/naive-tree/Cargo.lock
new file mode 100644
index 000000000..86f2ef0d6
--- /dev/null
+++ b/tests/src/naive-tree/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "naive-tree"
+version = "0.1.0"
diff --git a/tests/src/naive-tree/Cargo.toml b/tests/src/naive-tree/Cargo.toml
new file mode 100644
index 000000000..25f203d23
--- /dev/null
+++ b/tests/src/naive-tree/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "naive-tree"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "naive_tree"
+path = "src/naive-tree.rs"
diff --git a/tests/src/naive-tree/Makefile b/tests/src/naive-tree/Makefile
new file mode 100644
index 000000000..1e158b74d
--- /dev/null
+++ b/tests/src/naive-tree/Makefile
@@ -0,0 +1,10 @@
+.PHONY: all
+all: tests
+
+.PHONY: test
+test:
+	cargo test
+
+.PHONY: clean
+clean:
+	cargo clean
diff --git a/tests/src/naive-tree/aeneas-test-options b/tests/src/naive-tree/aeneas-test-options
new file mode 100644
index 000000000..a9153114b
--- /dev/null
+++ b/tests/src/naive-tree/aeneas-test-options
@@ -0,0 +1,2 @@
+[!lean] skip
+[lean] aeneas-args=-split-files -no-gen-lib-entry
\ No newline at end of file
diff --git a/tests/src/naive-tree/rust-toolchain b/tests/src/naive-tree/rust-toolchain
new file mode 100644
index 000000000..9460b1a82
--- /dev/null
+++ b/tests/src/naive-tree/rust-toolchain
@@ -0,0 +1,3 @@
+[toolchain]
+channel = "nightly-2023-06-02"
+components = [ "rustc-dev", "llvm-tools-preview" ]
diff --git a/tests/src/naive-tree/src/naive-tree.rs b/tests/src/naive-tree/src/naive-tree.rs
new file mode 100644
index 000000000..197276d71
--- /dev/null
+++ b/tests/src/naive-tree/src/naive-tree.rs
@@ -0,0 +1,174 @@
+//! Adapted from https://github.com/RaitoBezarius/avl-verification
+#![feature(register_tool)]
+#![register_tool(aeneas)]
+
+pub enum Ordering {
+    Less,
+    Equal,
+    Greater,
+}
+
+trait Ord {
+    fn cmp(&self, other: &Self) -> Ordering;
+}
+
+trait Bounded {
+    type Value;
+    fn max_value() -> Self::Value;
+    fn min_value() -> Self::Value;
+}
+
+struct Node<T> {
+    value: T,
+    left: Tree<T>,
+    right: Tree<T>,
+}
+
+type Tree<T> = Option<Box<Node<T>>>;
+
+struct TreeSet<T> {
+    root: Tree<T>,
+}
+
+impl<T: Ord> TreeSet<T> {
+    pub fn new() -> Self {
+        Self { root: None }
+    }
+
+    pub fn find(&self, value: T) -> bool {
+        let mut current_tree = &self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &current_node.right,
+                Ordering::Equal => return true,
+                Ordering::Greater => current_tree = &current_node.left,
+            }
+        }
+
+        false
+    }
+    pub fn insert(&mut self, value: T) -> bool {
+        let mut current_tree = &mut self.root;
+
+        while let Some(current_node) = current_tree {
+            match current_node.value.cmp(&value) {
+                Ordering::Less => current_tree = &mut current_node.right,
+                Ordering::Equal => return false,
+                Ordering::Greater => current_tree = &mut current_node.left,
+            }
+        }
+
+        *current_tree = Some(Box::new(Node {
+            value,
+            left: None,
+            right: None,
+        }));
+
+        true
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    impl Ord for i32 {
+        fn cmp(&self, other: &Self) -> Ordering {
+            if *self < *other {
+                Ordering::Less
+            } else if *self == *other {
+                Ordering::Equal
+            } else {
+                Ordering::Greater
+            }
+        }
+    }
+
+    impl Bounded for i32 {
+        type Value = i32;
+        fn min_value() -> i32 {
+            i32::MIN
+        }
+        fn max_value() -> i32 {
+            i32::MAX
+        }
+    }
+
+    impl<T: Bounded<Value = T> + Ord + Copy> Node<T> {
+        fn check_bst_inv(&self, min: T, max: T) -> bool {
+            matches!(self.value.cmp(&min), Ordering::Greater)
+                && matches!(self.value.cmp(&max), Ordering::Less)
+                && self
+                    .left
+                    .as_ref()
+                    .map_or(true, |left| left.check_bst_inv(min, self.value))
+                && self
+                    .right
+                    .as_ref()
+                    .map_or(true, |right| right.check_bst_inv(self.value, max))
+        }
+    }
+
+    impl<T: Bounded<Value = T> + Ord + Copy> TreeSet<T> {
+        fn check_bst_inv(&self) -> bool {
+            self.root
+                .as_ref()
+                .map_or(true, |r| r.check_bst_inv(T::min_value(), T::max_value()))
+        }
+    }
+
+    #[test]
+    fn unbalanced_right() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in 0..100 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(50),
+            "Unexpectedly failed to find the 50 value in the tree"
+        );
+
+        assert!(!t.find(-50), "Unexpectedly find the -50 value in the tree");
+    }
+
+    #[test]
+    fn unbalanced_left() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in -100..0 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(-50),
+            "Unexpectedly failed to find the -50 value in the tree"
+        );
+
+        assert!(!t.find(50), "Unexpectedly find the 50 value in the tree");
+    }
+
+    #[test]
+    fn right_left_unbalanced() {
+        let mut t: TreeSet<i32> = TreeSet::new();
+        for i in 0..100 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+        for i in -100..0 {
+            t.insert(i);
+            t.check_bst_inv();
+        }
+
+        assert!(
+            t.find(-50),
+            "Unexpectedly failed to find the -50 value in the tree"
+        );
+        assert!(
+            t.find(50),
+            "Unexpectedly failed to find the 50 value in the tree"
+        );
+    }
+}