diff --git a/src/util/rb_map.h b/src/util/rb_map.h
index 11283f23d..5ecd56473 100644
--- a/src/util/rb_map.h
+++ b/src/util/rb_map.h
@@ -36,6 +36,8 @@ public:
     bool contains(K const & k) const { return m_map.contains(mk_pair(k, T())); }
     void erase(K const & k) { m_map.erase(mk_pair(k, T())); }
 
+    unsigned get_rc() const { return m_map.get_rc(); }
+
     class ref {
         rb_map & m_map;
         K const &   m_key;
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index 514356966..30c501994 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -287,6 +287,8 @@ public:
     rb_tree & operator=(rb_tree const & s) { m_root = s.m_root; return *this; }
     rb_tree & operator=(rb_tree && s) { m_root = s.m_root; return *this; }
 
+    unsigned get_rc() const { return m_root ? m_root->get_rc() : 0; }
+
     void insert(T const & v) {
         m_root = set_black(insert(m_root.steal(), v));
         lean_assert(check_invariant());