diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h
index 18752eba0f4..45d5a5529d9 100644
--- a/src/util/sharing_map.h
+++ b/src/util/sharing_map.h
@@ -44,6 +44,12 @@ Author: Daniel Poetzl
   template <class keyT, class valueT, class hashT, class equalT> \
   CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \
     sharing_mapt<keyT, valueT, hashT, equalT>
+
+#define SHARING_MAPT3(T, CV, ST) \
+  template <class keyT, class valueT, class hashT, class equalT> \
+  template <class T> \
+  CV typename sharing_mapt<keyT, valueT, hashT, equalT>::ST \
+    sharing_mapt<keyT, valueT, hashT, equalT>
 // clang-format on
 
 // Note: Due to a bug in Visual Studio we need to add an additional "const"
@@ -124,11 +130,6 @@ template <class keyT,
 class sharing_mapt
 {
 public:
-  friend void sharing_map_interface_test();
-  friend void sharing_map_copy_test();
-  friend void sharing_map_collision_test();
-  friend void sharing_map_view_test();
-
   ~sharing_mapt()
   {
   }
@@ -291,6 +292,35 @@ class sharing_mapt
     delta_viewt &delta_view,
     const bool only_common = true) const;
 
+  /// Stats about sharing between several sharing map instances. An instance of
+  /// this class is returned by the get_sharing_map_stats_* functions.
+  ///
+  /// The num_nodes field gives the total number of nodes in the given maps.
+  /// Nodes that are part of n of the maps are counted n times.
+  ///
+  /// The num_unique_nodes field gives the number of unique nodes in the given
+  /// maps. A node that is part of several of the maps is only counted once.
+  ///
+  /// The num_leafs and num_unique_leafs fields are similar to the above but
+  /// only leafs are counted.
+  struct sharing_map_statst
+  {
+    std::size_t num_nodes = 0;
+    std::size_t num_unique_nodes = 0;
+    std::size_t num_leafs = 0;
+    std::size_t num_unique_leafs = 0;
+  };
+
+  template <class Iterator>
+  static sharing_map_statst get_sharing_stats(
+    Iterator begin,
+    Iterator end,
+    std::function<sharing_mapt &(const Iterator)> f =
+      [](const Iterator it) -> sharing_mapt & { return *it; });
+
+  template <class Iterator>
+  static sharing_map_statst get_sharing_stats_map(Iterator begin, Iterator end);
+
 protected:
   // helpers
 
@@ -317,6 +347,11 @@ class sharing_mapt
   void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view)
     const;
 
+  std::size_t count_unmarked_nodes(
+    bool leafs_only,
+    std::set<void *> &marked,
+    bool mark = true) const;
+
   // dummy element returned when no element was found
   static mapped_type dummy;
 
@@ -386,6 +421,167 @@ ::iterate(
   while(!stack.empty());
 }
 
+SHARING_MAPT(std::size_t)
+::count_unmarked_nodes(bool leafs_only, std::set<void *> &marked, bool mark)
+  const
+{
+  if(empty())
+    return 0;
+
+  unsigned count = 0;
+
+  typedef std::pair<unsigned, const baset *> stack_itemt;
+
+  std::stack<stack_itemt> stack;
+  stack.push({0, &map});
+
+  do
+  {
+    const stack_itemt &si = stack.top();
+
+    const unsigned depth = si.first;
+    const baset *bp = si.second;
+
+    stack.pop();
+
+    // internal node or container node
+    const innert *ip = static_cast<const innert *>(bp);
+    const unsigned use_count = ip->data.use_count();
+    void *raw_ptr = ip->data.get();
+
+    if(use_count >= 2)
+    {
+      if(marked.find(raw_ptr) != marked.end())
+      {
+        continue;
+      }
+
+      if(mark)
+      {
+        marked.insert(raw_ptr);
+      }
+    }
+
+    if(!leafs_only)
+    {
+      count++;
+    }
+
+    if(depth < steps) // internal
+    {
+      const to_mapt &m = ip->get_to_map();
+      SM_ASSERT(!m.empty());
+
+      for(const auto &item : m)
+      {
+        const innert *i = &item.second;
+        stack.push({depth + 1, i});
+      }
+    }
+    else // container
+    {
+      SM_ASSERT(depth == steps);
+
+      const leaf_listt &ll = ip->get_container();
+      SM_ASSERT(!ll.empty());
+
+      for(const auto &l : ll)
+      {
+        const unsigned use_count = l.data.use_count();
+        void *raw_ptr = l.data.get();
+
+        if(use_count >= 2)
+        {
+          if(marked.find(raw_ptr) != marked.end())
+          {
+            continue;
+          }
+
+          if(mark)
+          {
+            marked.insert(raw_ptr);
+          }
+        }
+
+        count++;
+      }
+    }
+  } while(!stack.empty());
+
+  return count;
+}
+
+/// Get sharing stats
+///
+/// Complexity:
+/// - Worst case: O(N * H * log(S))
+/// - Best case: O(N + H)
+///
+/// \param begin: begin iterator
+/// \param end: end iterator
+/// \param f: function applied to the iterator to get a sharing map
+/// \return: sharing stats
+SHARING_MAPT3(Iterator, , sharing_map_statst)
+::get_sharing_stats(
+  Iterator begin,
+  Iterator end,
+  std::function<sharing_mapt &(const Iterator)> f)
+{
+  std::set<void *> marked;
+  sharing_map_statst sms;
+
+  // We do a separate pass over the tree for each statistic. This is not very
+  // efficient but the function is intended only for diagnosis purposes anyways.
+
+  // number of nodes
+  for(Iterator it = begin; it != end; it++)
+  {
+    sms.num_nodes += f(it).count_unmarked_nodes(false, marked, false);
+  }
+
+  SM_ASSERT(marked.empty());
+
+  // number of unique nodes
+  for(Iterator it = begin; it != end; it++)
+  {
+    sms.num_unique_nodes += f(it).count_unmarked_nodes(false, marked, true);
+  }
+
+  marked.clear();
+
+  // number of leafs
+  for(Iterator it = begin; it != end; it++)
+  {
+    sms.num_leafs += f(it).count_unmarked_nodes(true, marked, false);
+  }
+
+  SM_ASSERT(marked.empty());
+
+  // number of unique leafs
+  for(Iterator it = begin; it != end; it++)
+  {
+    sms.num_unique_leafs += f(it).count_unmarked_nodes(true, marked, true);
+  }
+
+  return sms;
+}
+
+/// Get sharing stats
+///
+/// Complexity:
+/// - Worst case: O(N * H * log(S))
+/// - Best case: O(N + H)
+///
+/// \param begin: begin iterator of a map
+/// \param end: end iterator of a map
+/// \return: sharing stats
+SHARING_MAPT3(Iterator, , sharing_map_statst)
+::get_sharing_stats_map(Iterator begin, Iterator end)
+{
+  return get_sharing_stats<Iterator>(
+    begin, end, [](const Iterator it) -> sharing_mapt & { return it->second; });
+}
+
 /// Get a view of the elements in the map
 /// A view is a list of pairs with the components being const references to the
 /// keys and values in the map.
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index 88a7a53b042..09598506e76 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -129,6 +129,8 @@ SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset
 
   bool shares_with(const sharing_node_innert &other) const
   {
+    SN_ASSERT(data && other.data);
+
     return data == other.data;
   }
 
@@ -151,8 +153,6 @@ SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset
 
   d_it &write_internal()
   {
-    SN_ASSERT(data.use_count() > 0);
-
     if(data == empty_data)
     {
       data = make_shared_derived_u<SN_PTR_TYPE_ARGS>();
@@ -176,8 +176,6 @@ SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset
 
   d_ct &write_container()
   {
-    SN_ASSERT(data.use_count() > 0);
-
     if(data == empty_data)
     {
       data = make_shared_derived_v<SN_PTR_TYPE_ARGS>();
@@ -259,8 +257,9 @@ SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset
   leaft *place_leaf(const keyT &k, const valueT &v)
   {
     SN_ASSERT(is_container());
-
-    SN_ASSERT(as_const(this)->find_leaf(k) == nullptr);
+    // we need to check empty() first as the const version of find_leaf() must
+    // not be called on an empty node
+    SN_ASSERT(empty() || as_const(this)->find_leaf(k) == nullptr);
 
     leaf_listt &c = get_container();
     c.push_front(leaft(k, v));
diff --git a/unit/util/sharing_map.cpp b/unit/util/sharing_map.cpp
index 3116520ec80..e1bfda93e0b 100644
--- a/unit/util/sharing_map.cpp
+++ b/unit/util/sharing_map.cpp
@@ -6,16 +6,24 @@ Author: Daniel Poetzl
 
 \*******************************************************************/
 
-#define SHARING_MAP_INTERNAL_CHECKS
-#define SHARING_NODE_INTERNAL_CHECKS
+#define SM_INTERNAL_CHECKS
+#define SN_INTERNAL_CHECKS
 
 #include <climits>
 #include <random>
+#include <set>
 
 #include <testing-utils/catch.hpp>
 #include <util/sharing_map.h>
 
-typedef sharing_mapt<irep_idt, std::string, irep_id_hash> smt;
+class smt : public sharing_mapt<irep_idt, std::string, irep_id_hash>
+{
+  friend void sharing_map_interface_test();
+  friend void sharing_map_copy_test();
+  friend void sharing_map_collision_test();
+  friend void sharing_map_view_test();
+  friend void sharing_map_sharing_stats_test();
+};
 
 // helpers
 void fill(smt &sm)
@@ -248,6 +256,14 @@ void sharing_map_collision_test()
 
 void sharing_map_view_test()
 {
+  SECTION("View of empty map")
+  {
+    smt sm;
+    smt::viewt view;
+
+    sm.get_view(view);
+  }
+
   SECTION("View")
   {
     typedef std::pair<dstringt, std::string> pt;
@@ -365,6 +381,143 @@ void sharing_map_view_test()
   }
 }
 
+void sharing_map_sharing_stats_test()
+{
+  SECTION("count nodes")
+  {
+    std::set<void *> marked;
+    smt sm;
+    int count = 0;
+
+    count = sm.count_unmarked_nodes(false, marked, false);
+    REQUIRE(count == 0);
+
+    count = sm.count_unmarked_nodes(true, marked, false);
+    REQUIRE(count == 0);
+
+    sm.insert("i", "1");
+    count = sm.count_unmarked_nodes(false, marked, false);
+    REQUIRE(count == 8);
+
+    count = sm.count_unmarked_nodes(true, marked, false);
+    REQUIRE(count == 1);
+
+    sm.clear();
+    fill(sm);
+    count = sm.count_unmarked_nodes(true, marked, false);
+    REQUIRE(count == 3);
+  }
+
+  SECTION("marking")
+  {
+    std::set<void *> marked;
+    smt sm;
+
+    fill(sm);
+
+    sm.count_unmarked_nodes(false, marked, true);
+    REQUIRE(marked.empty());
+
+    smt sm2(sm);
+    sm.count_unmarked_nodes(false, marked, true);
+    REQUIRE(marked.size() == 1);
+
+    marked.clear();
+    smt sm3(sm);
+    sm3["x"];
+    sm.count_unmarked_nodes(false, marked, true);
+    REQUIRE(marked.size() >= 2);
+  }
+
+  SECTION("sharing stats")
+  {
+    std::vector<smt> v;
+    smt::sharing_map_statst sms;
+
+    SECTION("sharing stats no sharing")
+    {
+      v.emplace_back();
+      v.emplace_back();
+
+      REQUIRE(v.size() == 2);
+
+      // Empty maps
+      sms = smt::get_sharing_stats(v.begin(), v.end());
+      REQUIRE(sms.num_nodes == 0);
+      REQUIRE(sms.num_unique_nodes == 0);
+      REQUIRE(sms.num_leafs == 0);
+      REQUIRE(sms.num_unique_leafs == 0);
+
+      smt &sm1 = v.at(0);
+      smt &sm2 = v.at(1);
+
+      fill(sm1);
+      fill(sm2);
+
+      // Non-empty maps
+      sms = smt::get_sharing_stats(v.begin(), v.end());
+      REQUIRE(sms.num_leafs == 6);
+      REQUIRE(sms.num_unique_leafs == 6);
+    }
+
+    SECTION("sharing stats sharing 1")
+    {
+      smt sm1;
+      fill(sm1);
+      v.push_back(sm1);
+
+      smt sm2(sm1);
+      v.push_back(sm2);
+
+      sms = smt::get_sharing_stats(v.begin(), v.end());
+      REQUIRE(sms.num_leafs == 6);
+      REQUIRE(sms.num_unique_leafs == 3);
+    }
+
+    SECTION("sharing stats sharing 2")
+    {
+      smt sm1;
+      fill(sm1);
+      v.push_back(sm1);
+
+      smt sm2(sm1);
+      v.push_back(sm2);
+
+      smt sm3(sm1);
+      // new
+      sm3["x"];
+      v.push_back(sm3);
+
+      smt sm4(sm1);
+      // existing
+      sm4["i"];
+      v.push_back(sm4);
+
+      sms = smt::get_sharing_stats(v.begin(), v.end());
+      REQUIRE(sms.num_leafs == 13);
+      REQUIRE(sms.num_unique_leafs == 5);
+    }
+  }
+
+  SECTION("sharing stats map")
+  {
+    std::map<irep_idt, smt> m;
+
+    smt sm1;
+    fill(sm1);
+
+    smt sm2(sm1);
+
+    m["a"] = sm1;
+    m["b"] = sm2;
+
+    smt::sharing_map_statst sms;
+    sms = smt::get_sharing_stats_map(m.begin(), m.end());
+    REQUIRE(sms.num_leafs == 6);
+    REQUIRE(sms.num_unique_leafs == 3);
+  }
+}
+
 TEST_CASE("Sharing map interface")
 {
   sharing_map_interface_test();
@@ -384,3 +537,8 @@ TEST_CASE("Sharing map views")
 {
   sharing_map_view_test();
 }
+
+TEST_CASE("Sharing map sharing stats")
+{
+  sharing_map_sharing_stats_test();
+}
diff --git a/unit/util/sharing_node.cpp b/unit/util/sharing_node.cpp
index 470cf7beafd..7a5e81d9e42 100644
--- a/unit/util/sharing_node.cpp
+++ b/unit/util/sharing_node.cpp
@@ -2,7 +2,7 @@
 
 /// \file Tests for sharing-node utility
 
-#define SHARING_NODE_INTERNAL_CHECKS
+#define SN_INTERNAL_CHECKS
 
 #include <testing-utils/catch.hpp>
 #include <util/sharing_node.h>