diff --git a/src/tests/util/splay_tree.cpp b/src/tests/util/splay_tree.cpp
index 1293a76ee9..1b537a7ecb 100644
--- a/src/tests/util/splay_tree.cpp
+++ b/src/tests/util/splay_tree.cpp
@@ -66,7 +66,7 @@ static void tst1() {
     s.insert(34);
     std::cout << s2 << "\n";
     std::cout << s << "\n";
-    int const * v = s.find_memoize(11);
+    int const * v = s.splay_find(11);
     lean_assert(*v == 11);
     std::cout << s << "\n";
     lean_assert(!s.empty());
@@ -155,10 +155,20 @@ static void tst3() {
     lean_assert(out.str() == "1 3 5 10 ");
 }
 
+static void tst4() {
+    int_splay_tree s;
+    s.insert(10);
+    s.insert(20);
+    lean_assert(s.splay_find(30) == nullptr);
+    lean_assert(*(s.splay_find(20)) == 20);
+    lean_assert(*(s.splay_find(10)) == 10);
+}
+
 int main() {
     tst0();
     tst1();
     tst2();
     tst3();
+    tst4();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/splay_map.h b/src/util/splay_map.h
index b7759cc2fa..cc65ddee57 100644
--- a/src/util/splay_map.h
+++ b/src/util/splay_map.h
@@ -32,7 +32,7 @@ public:
     void insert(K const & k, T const & v) { m_map.insert(mk_pair(k, v)); }
     entry const * find(K const & k) const { return m_map.find(mk_pair(k, T())); }
     bool contains(K const & k) const { return m_map.contains(mk_pair(k, T())); }
-    entry const * find_memoize(K const & k) { return m_map.contains(mk_pair(k, T())); }
+    entry const * splay_find(K const & k) { return m_map.contains(mk_pair(k, T())); }
     void erase(K const & k) { m_map.erase(mk_pair(k, T())); }
 
     class ref {
diff --git a/src/util/splay_tree.h b/src/util/splay_tree.h
index 04565c3800..7b5d5accbe 100644
--- a/src/util/splay_tree.h
+++ b/src/util/splay_tree.h
@@ -367,10 +367,10 @@ public:
 
     /**
         \brief Similar to \c find, but the splay tree is reorganized.
-        If <tt>find(v)</tt> is invoked after <tt>find_memoize(v)</tt>, then the cost will be O(1).
+        If <tt>find(v)</tt> is invoked after <tt>splay_find(v)</tt>, then the cost will be O(1).
         The idea is to move recently accessed elements close to the root.
     */
-    T const * find_memoize(T const & v) {
+    T const * splay_find(T const & v) {
         if (pull(v)) {
             lean_assert(cmp(m_ptr->m_value, v) == 0);
             return &(m_ptr->m_value);