diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h
new file mode 100644
index 00000000000..23f08d0bb06
--- /dev/null
+++ b/src/util/sharing_map.h
@@ -0,0 +1,832 @@
+/*******************************************************************\
+
+Module: Sharing map
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SHARING_MAP_H
+#define CPROVER_UTIL_SHARING_MAP_H
+
+#include <string>
+#include <stack>
+#include <vector>
+#include <map>
+#include <stdexcept>
+#include <functional>
+#include <memory>
+#include <iosfwd>
+#include <cassert>
+
+#include <util/string2int.h>
+#include <util/threeval.h>
+#include <util/irep.h>
+#include <util/sharing_node.h>
+
+#define _sm_assert(b) assert(b)
+//#define _sm_assert(b)
+
+#define SHARING_MAPT(R) \
+  template <class keyT, class valueT, class hashT, class predT> \
+  R sharing_mapt<keyT, valueT, hashT, predT>
+
+#define SHARING_MAPT2(CV, ST) \
+  template <class keyT, class valueT, class hashT, class predT> \
+  CV typename sharing_mapt<keyT, valueT, hashT, predT>::ST \
+  sharing_mapt<keyT, valueT, hashT, predT>
+
+template <
+  class keyT,
+  class valueT,
+  class hashT=std::hash<keyT>,
+  class predT=std::equal_to<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()
+  {
+  }
+
+  typedef keyT key_type;
+  typedef valueT mapped_type;
+  typedef std::pair<const key_type, mapped_type> value_type;
+
+  typedef hashT hash;
+  typedef predT key_equal;
+
+  typedef sharing_mapt<key_type, mapped_type, hash, key_equal> self_type;
+  typedef sharing_nodet<key_type, mapped_type, key_equal> node_type;
+
+  typedef size_t size_type;
+
+  typedef const std::pair<const mapped_type &, const bool> const_find_type;
+  typedef const std::pair<mapped_type &, const bool> find_type;
+
+  typedef std::vector<key_type> keyst;
+
+  typedef typename node_type::subt subt;
+  typedef typename node_type::containert containert;
+
+  // key-value map
+  node_type map;
+
+  // number of elements in the map
+  size_type num=0;
+
+  // dummy element returned when no element was found
+  static mapped_type dummy;
+
+  // compile-time configuration
+
+  static const std::string not_found_msg;
+
+  static const size_t bits;
+  static const size_t chunk;
+
+  static const size_t mask;
+  static const size_t steps;
+
+  // interface
+
+  size_type erase(
+    const key_type &k,
+    const tvt &key_exists=tvt::unknown());
+
+  size_type erase_all(
+    const keyst &ks,
+    const tvt &key_exists=tvt::unknown()); // applies to all keys
+
+  // return true if element was inserted
+  const_find_type insert(
+    const key_type &k,
+    const mapped_type &v,
+    const tvt &key_exists=tvt::unknown());
+
+  const_find_type insert(
+    const value_type &p,
+    const tvt &key_exists=tvt::unknown());
+
+  find_type place(
+    const key_type &k,
+    const mapped_type &v);
+
+  find_type place(
+    const value_type &p);
+
+  find_type find(
+    const key_type &k,
+    const tvt &key_exists=tvt::unknown());
+
+  const_find_type find(const key_type &k) const;
+
+  mapped_type &at(
+    const key_type &k,
+    const tvt &key_exists=tvt::unknown());
+
+  const mapped_type &at(const key_type &k) const;
+
+  mapped_type &operator[](const key_type &k);
+
+  void swap(self_type &other)
+  {
+    map.swap(other.map);
+
+    size_t tmp=num;
+    num=other.num;
+    other.num=tmp;
+  }
+
+  size_type size() const
+  {
+    return num;
+  }
+
+  bool empty() const
+  {
+    return num==0;
+  }
+
+  void clear()
+  {
+    map.clear();
+    num=0;
+  }
+
+  bool has_key(const key_type &k) const
+  {
+    return get_leaf_node(k)!=nullptr;
+  }
+
+  // views
+
+  typedef std::pair<const key_type &, const mapped_type &> view_itemt;
+  typedef std::vector<view_itemt> viewt;
+
+  class delta_view_itemt
+  {
+  public:
+    delta_view_itemt(
+      const bool in_both,
+      const key_type &k,
+      const mapped_type &m,
+      const mapped_type &other_m) :
+        in_both(in_both),
+        k(k),
+        m(m),
+        other_m(other_m) {}
+
+    // if true key is in both maps, if false key is only in the map
+    // from which the view was obtained
+    const bool in_both;
+
+    const key_type &k;
+
+    const mapped_type &m;
+    const mapped_type &other_m;
+  };
+
+  typedef std::vector<delta_view_itemt> delta_viewt;
+
+  void get_view(viewt &view) const;
+
+  void get_delta_view(
+    const self_type &other,
+    delta_viewt &delta_view,
+    const bool only_common=true) const;
+
+protected:
+  // helpers
+
+  node_type *get_container_node(const key_type &k);
+  const node_type *get_container_node(const key_type &k) const;
+
+  const node_type *get_leaf_node(const key_type &k) const;
+
+  void gather_all(const node_type &n, delta_viewt &delta_view) const;
+};
+
+/*******************************************************************\
+
+Function: get_view
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT(void)::get_view(viewt &view) const
+{
+  assert(view.empty());
+
+  std::stack<const node_type *> stack;
+
+  if(empty())
+    return;
+
+  stack.push(&map);
+
+  do
+  {
+    const node_type *n=stack.top();
+    stack.pop();
+
+    if(n->is_container())
+    {
+      for(const auto &child : n->get_container())
+      {
+        view.push_back(view_itemt(child.get_key(), child.get_value()));
+      }
+    }
+    else
+    {
+      assert(n->is_internal());
+
+      for(const auto &child : n->get_sub())
+      {
+        stack.push(&child.second);
+      }
+    }
+  }
+  while(!stack.empty());
+}
+
+/*******************************************************************\
+
+Function: gather_all
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT(void)::gather_all(const node_type &n, delta_viewt &delta_view)
+  const
+{
+  std::stack<const node_type *> stack;
+  stack.push(&n);
+
+  do
+  {
+    const node_type *n=stack.top();
+    stack.pop();
+
+    if(n->is_container())
+    {
+      for(const auto &child : n->get_container())
+      {
+        delta_view.push_back(
+          delta_view_itemt(
+            false,
+            child.get_key(),
+            child.get_value(),
+            dummy));
+      }
+    }
+    else
+    {
+      assert(n->is_internal());
+
+      for(const auto &child : n->get_sub())
+      {
+        stack.push(&child.second);
+      }
+    }
+  }
+  while(!stack.empty());
+}
+
+/*******************************************************************\
+
+Function: get_delta_view
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT(void)::get_delta_view(
+  const self_type &other,
+  delta_viewt &delta_view,
+  const bool only_common) const
+{
+  assert(delta_view.empty());
+
+  typedef std::pair<const node_type *, const node_type *> stack_itemt;
+  std::stack<stack_itemt> stack;
+
+  if(empty())
+    return;
+
+  if(other.empty())
+  {
+    if(!only_common)
+    {
+      gather_all(map, delta_view);
+    }
+    return;
+  }
+
+  stack.push(stack_itemt(&map, &other.map));
+
+  do
+  {
+    const stack_itemt si=stack.top();
+    stack.pop();
+
+    const node_type *n1=si.first;
+    const node_type *n2=si.second;
+
+    if(n1->is_internal())
+    {
+      _sn_assert(n2->is_internal());
+
+      for(const auto &child : n1->get_sub())
+      {
+        const node_type *p;
+
+        p=n2->find_child(child.first);
+        if(p==nullptr)
+        {
+          if(!only_common)
+          {
+            gather_all(child.second, delta_view);
+          }
+        }
+        else if(!child.second.shares_with(*p))
+        {
+          stack.push(stack_itemt(&child.second, p));
+        }
+      }
+    }
+    else if(n1->is_container())
+    {
+      _sn_assert(n2->is_container());
+
+      for(const auto &l1 : n1->get_container())
+      {
+        const key_type &k1=l1.get_key();
+        bool found=false;
+
+        for(const auto &l2 : n2->get_container())
+        {
+          const key_type &k2=l2.get_key();
+
+          if(l1.shares_with(l2))
+          {
+            found=true;
+            break;
+          }
+
+          if(key_equal()(k1, k2))
+          {
+            delta_view.push_back(
+              delta_view_itemt(
+                true,
+                k1,
+                l1.get_value(),
+                l2.get_value()));
+
+            found=true;
+            break;
+          }
+        }
+
+        if(!only_common && !found)
+        {
+          delta_view.push_back(
+            delta_view_itemt(
+              false,
+              l1.get_key(),
+              l1.get_value(),
+              dummy));
+        }
+      }
+    }
+    else
+    {
+      assert(false);
+    }
+  }
+  while(!stack.empty());
+}
+
+/*******************************************************************\
+
+Function: get_container_node
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, node_type *)::get_container_node(const key_type &k)
+{
+  size_t key=hash()(k);
+  node_type *p=&map;
+
+  for(unsigned i=0; i<steps; i++)
+  {
+    unsigned bit=key&mask;
+    key>>=chunk;
+
+    p=p->add_child(bit);
+  }
+
+  return p;
+}
+
+/*******************************************************************\
+
+Function: get_container_node
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(const, node_type *)::get_container_node(const key_type &k) const
+{
+  size_t key=hash()(k);
+  const node_type *p=&map;
+
+  for(unsigned i=0; i<steps; i++)
+  {
+    unsigned bit=key&mask;
+    key>>=chunk;
+
+    p=p->find_child(bit);
+    if(p==nullptr)
+      return nullptr;
+  }
+
+  assert(p->is_container());
+
+  return p;
+}
+
+/*******************************************************************\
+
+Function: get_leaf_node
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(const, node_type *)::get_leaf_node(const key_type &k) const
+{
+  const node_type *p=get_container_node(k);
+  if(p==nullptr)
+    return nullptr;
+
+  p=p->find_leaf(k);
+
+  return p;
+}
+
+/*******************************************************************\
+
+Function: erase
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, size_type)::erase(
+  const key_type &k,
+  const tvt &key_exists)
+{
+  assert(!key_exists.is_false());
+
+  // check if key exists
+  if(key_exists.is_unknown() && !has_key(k))
+    return 0;
+
+  node_type *del=nullptr;
+  unsigned del_bit;
+
+  size_t key=hash()(k);
+  node_type *p=&map;
+
+  for(unsigned i=0; i<steps; i++)
+  {
+    unsigned bit=key&mask;
+    key>>=chunk;
+
+    const subt &sub=as_const(p)->get_sub();
+    if(sub.size()>1 || del==nullptr)
+    {
+      del=p;
+      del_bit=bit;
+    }
+
+    p=p->add_child(bit);
+  }
+
+  _sm_assert(p->is_container());
+
+  {
+    const containert &c=as_const(p)->get_container();
+
+    if(c.size()==1)
+    {
+      del->remove_child(del_bit);
+      num--;
+      return 1;
+    }
+  }
+
+  containert &c=p->get_container();
+  _sm_assert(c.size()>1);
+  p->remove_leaf(k);
+  num--;
+
+  return 1;
+}
+
+/*******************************************************************\
+
+Function: erase_all
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, size_type)::erase_all(
+  const keyst &ks,
+  const tvt &key_exists)
+{
+  size_type cnt=0;
+
+  for(const key_type &k : ks)
+  {
+    cnt+=erase(k, key_exists);
+  }
+
+  return cnt;
+}
+
+/*******************************************************************\
+
+Function: insert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, const_find_type)::insert(
+  const key_type &k,
+  const mapped_type &m,
+  const tvt &key_exists)
+{
+  _sn_assert(!key_exists.is_true());
+
+  if(key_exists.is_unknown())
+  {
+    const node_type *p=as_const(this)->get_leaf_node(k);
+    if(p!=nullptr)
+      return const_find_type(p->get_value(), false);
+  }
+
+  node_type *p=get_container_node(k);
+  _sn_assert(p!=nullptr);
+
+  p=p->place_leaf(k, m);
+  num++;
+
+  return const_find_type(as_const(p)->get_value(), true);
+}
+
+/*******************************************************************\
+
+Function: insert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, const_find_type)::insert(
+  const value_type &p,
+  const tvt &key_exists)
+{
+  return insert(p.first, p.second, key_exists);
+}
+
+/*******************************************************************\
+
+Function: place
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, find_type)::place(
+  const key_type &k,
+  const mapped_type &m)
+{
+  node_type *c=get_container_node(k);
+  _sm_assert(c!=nullptr);
+
+  node_type *p=c->find_leaf(k);
+
+  if(p!=nullptr)
+    return find_type(p->get_value(), false);
+
+  p=c->place_leaf(k, m);
+  num++;
+
+  return find_type(p->get_value(), true);
+}
+
+/*******************************************************************\
+
+Function: place
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, find_type)::place(
+  const value_type &p)
+{
+  return place(p.first, p.second);
+}
+
+/*******************************************************************\
+
+Function: find
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, find_type)::find(
+  const key_type &k,
+  const tvt &key_exists)
+{
+  _sm_assert(!key_exists.is_false());
+
+  if(key_exists.is_unknown() && !has_key(k))
+    return find_type(dummy, false);
+
+  node_type *p=get_container_node(k);
+  _sm_assert(p!=nullptr);
+
+  p=p->find_leaf(k);
+  _sm_assert(p!=nullptr);
+
+  return find_type(p->get_value(), true);
+
+}
+
+/*******************************************************************\
+
+Function: find
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, const_find_type)::find(const key_type &k) const
+{
+  const node_type *p=get_leaf_node(k);
+
+  if(p==nullptr)
+    return const_find_type(dummy, false);
+
+  return const_find_type(p->get_value(), true);
+}
+
+/*******************************************************************\
+
+Function: at
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, mapped_type &)::at(
+  const key_type &k,
+  const tvt &key_exists)
+{
+  find_type r=find(k, key_exists);
+
+  if(!r.second)
+    throw std::out_of_range(not_found_msg);
+
+  return r.first;
+}
+
+/*******************************************************************\
+
+Function: at
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(const, mapped_type &)::at(const key_type &k) const
+{
+  const_find_type r=find(k);
+  if(!r.second)
+    throw std::out_of_range(not_found_msg);
+
+  return r.first;
+}
+
+/*******************************************************************\
+
+Function: operator[]
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+SHARING_MAPT2(, mapped_type &)::operator[](const key_type &k)
+{
+  return place(k, mapped_type()).first;
+}
+
+// static constants
+
+SHARING_MAPT(const std::string)::not_found_msg="key not found";
+
+// config
+SHARING_MAPT(const size_t)::bits=18;
+SHARING_MAPT(const size_t)::chunk=3;
+
+// derived config
+SHARING_MAPT(const size_t)::mask=0xffff>>(16-chunk);
+SHARING_MAPT(const size_t)::steps=bits/chunk;
+
+SHARING_MAPT2(, mapped_type)::dummy;
+
+#endif
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
new file mode 100644
index 00000000000..1e3d29a413e
--- /dev/null
+++ b/src/util/sharing_node.h
@@ -0,0 +1,346 @@
+/*******************************************************************\
+
+Module: Sharing node
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SHARING_NODE_H
+#define CPROVER_UTIL_SHARING_NODE_H
+
+#include <list>
+#include <map>
+#include <memory>
+#include <cassert>
+
+#define _sn_assert(b) assert(b)
+//#define _sn_assert(b)
+
+template <class T>
+const T *as_const(T *t)
+{
+  return t;
+}
+
+template <
+  class keyT,
+  class valueT,
+  class predT=std::equal_to<keyT>,
+  bool no_sharing=false>
+class sharing_nodet
+{
+public:
+  friend void sharing_node_test();
+
+  typedef keyT key_type;
+  typedef valueT mapped_type;
+
+  typedef predT key_equal;
+
+  typedef sharing_nodet<key_type, mapped_type, key_equal> self_type;
+
+  typedef std::map<unsigned, self_type> subt;
+  typedef std::list<self_type> containert;
+
+  typedef const std::pair<const self_type &, const bool> const_find_type;
+  typedef const std::pair<self_type &, const bool> find_type;
+
+  sharing_nodet() : data(empty_data)
+  {
+    _sn_assert(data.use_count()>=2);
+  }
+
+  sharing_nodet(const key_type &k, const mapped_type &m) : data(empty_data)
+  {
+    _sn_assert(data.use_count()>=2);
+
+    dt &d=write();
+
+    _sn_assert(d.k==nullptr);
+    d.k=std::make_shared<key_type>(k);
+
+    _sn_assert(d.m==nullptr);
+    d.m.reset(new mapped_type(m));
+  }
+
+  sharing_nodet(const self_type &other)
+  {
+#ifdef SM_NO_SHARING
+    data=std::make_shared<dt>(*other.data);
+#else
+    if(no_sharing)
+    {
+      data=std::make_shared<dt>(*other.data);
+    }
+    else
+    {
+      data=other.data;
+    }
+#endif
+  }
+
+  // check type of node
+
+  bool is_empty() const
+  {
+    _sn_assert(is_well_formed());
+    return data==empty_data;
+  }
+
+  bool is_internal() const
+  {
+    _sn_assert(is_well_formed());
+    _sn_assert(!is_empty());
+    return !get_sub().empty();
+  }
+
+  bool is_container() const
+  {
+    _sn_assert(is_well_formed());
+    _sn_assert(!is_empty());
+    return !get_container().empty();
+  }
+
+  bool is_leaf() const
+  {
+    _sn_assert(is_well_formed());
+    _sn_assert(!is_empty());
+    return read().is_leaf();
+  }
+
+  // accessors
+
+  const key_type &get_key() const
+  {
+    _sn_assert(is_leaf());
+    return *read().k;
+  }
+
+  const mapped_type &get_value() const
+  {
+    _sn_assert(is_leaf());
+    return *read().m;
+  }
+
+  mapped_type &get_value()
+  {
+    _sn_assert(is_leaf());
+    return *write().m;
+  }
+
+  subt &get_sub()
+  {
+    return write().sub;
+  }
+
+  const subt &get_sub() const
+  {
+    return read().sub;
+  }
+
+  containert &get_container()
+  {
+    return write().con;
+  }
+
+  const containert &get_container() const
+  {
+    return read().con;
+  }
+
+  // internal nodes
+
+  const self_type *find_child(const unsigned n) const
+  {
+    const subt &s=get_sub();
+    typename subt::const_iterator it=s.find(n);
+
+    if(it!=s.end())
+      return &it->second;
+
+    return nullptr;
+  }
+
+  self_type *add_child(const unsigned n)
+  {
+    subt &s=get_sub();
+    return &s[n];
+  }
+
+  void remove_child(const unsigned n)
+  {
+    subt &s=get_sub();
+    size_t r=s.erase(n);
+
+    _sn_assert(r==1);
+  }
+
+  // container nodes
+
+  const self_type *find_leaf(const key_type &k) const
+  {
+    const containert &c=get_container();
+
+    for(const auto &n : c)
+    {
+      if(key_equal()(n.get_key(), k))
+        return &n;
+    }
+
+    return nullptr;
+  }
+
+  self_type *find_leaf(const key_type &k)
+  {
+    containert &c=get_container();
+
+    for(auto &n : c)
+    {
+      if(key_equal()(n.get_key(), k))
+        return &n;
+    }
+
+    return nullptr;
+  }
+
+  // add leaf, key must not exist yet
+  self_type *place_leaf(const key_type &k, const mapped_type &m)
+  {
+    _sn_assert(as_const(this)->find_leaf(k)==nullptr);
+
+    containert &c=get_container();
+    c.push_back(self_type(k, m));
+
+    return &c.back();
+  }
+
+  // remove leaf, key must exist
+  void remove_leaf(const key_type &k)
+  {
+    containert &c=get_container();
+
+    for(typename containert::const_iterator it=c.begin();
+        it!=c.end(); it++)
+    {
+      const self_type &n=*it;
+
+      if(key_equal()(n.get_key(), k))
+      {
+        c.erase(it);
+        return;
+      }
+    }
+
+    assert(false);
+  }
+
+  // misc
+
+  void clear()
+  {
+    *this=self_type();
+  }
+
+  bool shares_with(const self_type &other) const
+  {
+    return data==other.data;
+  }
+
+  void swap(self_type &other)
+  {
+    data.swap(other.data);
+  }
+
+protected:
+  class dt
+  {
+  public:
+    dt() {}
+
+    dt(const dt &d) : k(d.k), sub(d.sub), con(d.con)
+    {
+      if(d.is_leaf())
+      {
+        _sn_assert(m==nullptr);
+        m.reset(new mapped_type(*d.m));
+      }
+    }
+
+    bool is_leaf() const
+    {
+      _sn_assert(k==nullptr || m!=nullptr);
+      return k!=nullptr;
+    }
+
+    std::shared_ptr<key_type> k;
+    std::unique_ptr<mapped_type> m;
+
+    subt sub;
+    containert con;
+  };
+
+  const dt &read() const
+  {
+    return *data;
+  }
+
+  dt &write()
+  {
+    detach();
+    return *data;
+  }
+
+  void detach()
+  {
+    _sn_assert(data.use_count()>0);
+
+    if(data==empty_data)
+      data=std::make_shared<dt>();
+    else if(data.use_count()>1)
+      data=std::make_shared<dt>(*data);
+
+    _sn_assert(data.use_count()==1);
+  }
+
+  bool is_well_formed() const
+  {
+    if(data==nullptr)
+      return false;
+
+    const dt &d=*data;
+
+    bool b;
+
+    // empty node
+    b=data==empty_data;
+    // internal node
+    b|=d.k==nullptr && d.m==nullptr && get_container().empty() &&
+       !get_sub().empty();
+    // container node
+    b|=d.k==nullptr && d.m==nullptr && !get_container().empty() &&
+       get_sub().empty();
+    // leaf node
+    b|=d.k!=nullptr && d.m!=nullptr && get_container().empty() &&
+       get_sub().empty();
+
+    return b;
+  }
+
+  std::shared_ptr<dt> data;
+  static std::shared_ptr<dt> empty_data;
+
+  // dummy node returned when node was not found
+  static sharing_nodet dummy;
+};
+
+template <class keyT, class valueT, class predT, bool no_sharing>
+std::shared_ptr<typename sharing_nodet<keyT, valueT, predT, no_sharing>::dt>
+  sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data(
+    new sharing_nodet<keyT, valueT, predT, no_sharing>::dt());
+
+template <class keyT, class valueT, class predT, bool no_sharing>
+sharing_nodet<keyT, valueT, predT, no_sharing>
+  sharing_nodet<keyT, valueT, predT, no_sharing>::dummy;
+
+#endif
diff --git a/unit/Makefile b/unit/Makefile
index 0b442445a0f..007ebd3c70d 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -1,6 +1,8 @@
 SRC = cpp_parser.cpp cpp_scanner.cpp elf_reader.cpp float_utils.cpp \
       ieee_float.cpp json.cpp miniBDD.cpp osx_fat_reader.cpp \
-      smt2_parser.cpp wp.cpp string_utils.cpp
+      smt2_parser.cpp wp.cpp string_utils.cpp \
+      sharing_map.cpp \
+      sharing_node.cpp
 
 INCLUDES= -I ../src/
 
@@ -59,3 +61,9 @@ wp$(EXEEXT): wp$(OBJEXT)
 string_utils$(EXEEXT): string_utils$(OBJEXT)
 	$(LINKBIN)
 
+sharing_map$(EXEEXT): sharing_map$(OBJEXT)
+	$(LINKBIN)
+
+sharing_node$(EXEEXT): sharing_node$(OBJEXT)
+	$(LINKBIN)
+
diff --git a/unit/sharing_map.cpp b/unit/sharing_map.cpp
new file mode 100644
index 00000000000..9911f460855
--- /dev/null
+++ b/unit/sharing_map.cpp
@@ -0,0 +1,336 @@
+#include <iostream>
+#include <cassert>
+
+#include <util/sharing_map.h>
+
+typedef sharing_mapt<irep_idt, std::string, irep_id_hash> smt;
+
+// helpers
+void fill(smt &sm)
+{
+  sm.insert("i", "0");
+  sm.insert("j", "1");
+  sm.insert("k", "2");
+}
+
+void fill2(smt &sm)
+{
+  sm.insert("l", "3");
+  sm.insert("m", "4");
+  sm.insert("n", "5");
+}
+
+// tests
+
+void sharing_map_interface_test()
+{
+  std::cout << "Running interface test" << std::endl;
+
+  // empty map
+  {
+    smt sm;
+
+    assert(sm.empty());
+    assert(sm.size()==0);
+    assert(!sm.has_key("i"));
+  }
+
+  // insert elements
+  {
+    smt sm;
+
+    smt::const_find_type r1=sm.insert(std::make_pair("i", "0"));
+    assert(r1.second);
+
+    smt::const_find_type r2=sm.insert("j", "1");
+    assert(r2.second);
+
+    smt::const_find_type r3=sm.insert(std::make_pair("i", "0"));
+    assert(!r3.second);
+
+    assert(sm.size()==2);
+    assert(!sm.empty());
+  }
+
+  // place elements
+  {
+    smt sm1;
+    smt sm2(sm1);
+
+    smt::find_type r1=sm1.place("i", "0");
+    assert(r1.second);
+    assert(!sm2.has_key("i"));    
+
+    std::string &s1=r1.first;
+    s1="1";
+
+    assert(sm1.at("i")=="1");
+  }
+
+  // retrieve elements
+  {
+    smt sm;
+    sm.insert("i", "0");
+    sm.insert("j", "1");
+
+    const smt &sm2=sm;
+
+    std::string s;
+    s=sm2.at("i");
+    assert(s=="0");
+
+    try {
+      sm2.at("k");
+      assert(false);
+    } catch (...) {}
+
+    s=sm2.at("j");
+    assert(s=="1");
+
+    assert(sm.has_key("i"));
+    assert(sm.has_key("j"));
+    assert(!sm.has_key("k"));
+
+    std::string &s2=sm.at("i");
+    s2="3";
+    assert(sm2.at("i")=="3");
+
+    assert(sm.size()==2);
+
+    smt::find_type r=sm.find("i");
+    assert(r.second);
+    r.first="4";
+    assert(sm2.at("i")=="4");
+
+    smt::const_find_type rc=sm2.find("k");
+    assert(!rc.second);
+  }
+
+  // remove elements
+  {
+    smt sm;
+    sm.insert("i", "0");
+    sm.insert("j", "1");
+
+    assert(sm.erase("k")==0);
+    assert(sm.size()==2);
+
+    assert(sm.erase("i")==1);
+    assert(!sm.has_key("i"));
+
+    assert(sm.erase("j")==1);
+    assert(!sm.has_key("j"));
+
+    sm.insert("i", "0");
+    sm.insert("j", "1");
+
+    smt sm3(sm);
+  
+    assert(sm.has_key("i"));
+    assert(sm.has_key("j"));
+    assert(sm3.has_key("i"));
+    assert(sm3.has_key("j"));
+
+    sm.erase("i");
+
+    assert(!sm.has_key("i"));
+    assert(sm.has_key("j"));
+
+    assert(sm3.has_key("i"));
+    assert(sm3.has_key("j"));
+
+    sm3.erase("i");
+    assert(!sm3.has_key("i"));
+  }
+
+  // operator[]
+  {
+    smt sm;
+
+    sm["i"];
+    assert(sm.has_key("i"));
+
+    sm["i"]="0";
+    assert(sm.at("i")=="0");
+
+    sm["j"]="1";
+    assert(sm.at("j")=="1");
+  }
+}
+
+void sharing_map_copy_test()
+{
+  std::cout << "Running copy test" << std::endl;
+
+  smt sm1;
+  const smt &sm2=sm1;
+
+  fill(sm1);
+
+  assert(sm2.find("i").first=="0");
+  assert(sm2.find("j").first=="1");
+  assert(sm2.find("k").first=="2");
+
+  smt sm3=sm1;
+  const smt &sm4=sm3;
+
+  assert(sm3.erase("l")==0);
+  assert(sm3.erase("i")==1);
+
+  assert(!sm4.has_key("i"));
+  sm3.place("i", "3");
+  assert(sm4.find("i").first=="3");
+}
+
+class some_keyt
+{
+public:
+  some_keyt(size_t s) : s(s)
+  {
+  }
+
+  size_t s;
+
+  bool operator==(const some_keyt &other) const
+  {
+    return s==other.s;
+  }
+};
+
+class some_key_hash
+{
+public:
+  size_t operator()(const some_keyt &k) const
+  {
+    return k.s & 0x3;
+  }
+};
+
+void sharing_map_collision_test()
+{
+  std::cout << "Running collision test" << std::endl;
+
+  typedef sharing_mapt<some_keyt, std::string, some_key_hash> smt;
+
+  smt sm;
+
+  sm.insert(0, "a");
+  sm.insert(8, "b");
+  sm.insert(16, "c");
+
+  sm.insert(1, "d");
+  sm.insert(2, "e");
+
+  sm.erase(8);
+
+  assert(sm.has_key(0));
+  assert(sm.has_key(16));
+
+  assert(sm.has_key(1));
+  assert(sm.has_key(2));
+
+  assert(!sm.has_key(8));
+}
+
+void sharing_map_view_test()
+{
+  std::cout << "Running view test" << std::endl;
+
+  // view test
+  {
+    smt sm;
+  
+    fill(sm);
+  
+    smt::viewt view;
+    sm.get_view(view);
+
+    assert(view.size()==3);
+  }
+
+  // delta view test (no sharing, same keys)
+  {
+    smt sm1;
+    fill(sm1);
+
+    smt sm2;
+    fill(sm2);
+
+    smt::delta_viewt delta_view;
+
+    sm1.get_delta_view(sm2, delta_view);
+    assert(delta_view.size()==3);
+
+    delta_view.clear();
+    sm1.get_delta_view(sm2, delta_view, false);
+    assert(delta_view.size()==3);
+  }
+
+  // delta view test (all shared, same keys)
+  {
+    smt sm1;
+    fill(sm1);
+
+    smt sm2(sm1);
+    
+    smt::delta_viewt delta_view;
+
+    sm1.get_delta_view(sm2, delta_view);
+    assert(delta_view.size()==0);
+
+    delta_view.clear();
+    sm1.get_delta_view(sm2, delta_view, false);
+    assert(delta_view.size()==0);
+  }
+
+  // delta view test (some sharing, same keys)
+  {
+    smt sm1;
+    fill(sm1);
+
+    smt sm2(sm1);
+    auto r=sm2.find("i");
+    assert(r.second);
+    r.first="3";
+    
+    smt::delta_viewt delta_view;
+
+    sm1.get_delta_view(sm2, delta_view);
+    assert(delta_view.size()>0); // not everything is shared
+    assert(delta_view.size()<3); // there is some sharing
+
+    delta_view.clear();
+    sm1.get_delta_view(sm2, delta_view, false);
+    assert(delta_view.size()>0); // not everything is shared
+    assert(delta_view.size()<3); // there is some sharing
+  }
+
+  // delta view test (no sharing, different keys)
+  {
+    smt sm1;
+    fill(sm1);
+
+    smt sm2;
+    fill2(sm2);
+
+    smt::delta_viewt delta_view;
+
+    sm1.get_delta_view(sm2, delta_view);
+    assert(delta_view.size()==0);
+
+    delta_view.clear();
+    sm1.get_delta_view(sm2, delta_view, false);
+    assert(delta_view.size()==3);
+  }
+}
+
+int main()
+{
+  sharing_map_interface_test();
+  sharing_map_copy_test();
+  sharing_map_collision_test();
+  sharing_map_view_test();
+
+  return 0;
+}
+
diff --git a/unit/sharing_node.cpp b/unit/sharing_node.cpp
new file mode 100644
index 00000000000..2d256b8dd45
--- /dev/null
+++ b/unit/sharing_node.cpp
@@ -0,0 +1,129 @@
+#include <iostream>
+#include <cassert>
+
+#include <util/sharing_node.h>
+
+void sharing_node_test()
+{
+  std::cout << "Running sharing node test" << std::endl;
+
+  typedef sharing_nodet<std::string, std::string> snt;
+
+  // internal node test
+  {
+    snt sn1;
+    const snt &sn2=sn1;
+
+    const snt *p2;
+
+    assert(sn1.is_empty());
+
+    sn1.add_child(0);
+    sn1.add_child(1);
+    sn1.add_child(2);
+
+    assert(!sn2.is_empty());
+    assert(sn2.is_internal());
+    assert(!sn2.is_container());
+    assert(!sn2.is_leaf());
+
+    assert(sn2.get_sub().size()==3);
+
+    p2=sn2.find_child(0);
+    assert(p2!=nullptr);
+
+    p2=sn1.find_child(0);
+    assert(p2!=nullptr);
+
+    p2=sn2.find_child(3);
+    assert(p2==nullptr);
+
+    p2=sn1.find_child(3);
+    assert(p2==nullptr);
+
+    sn1.remove_child(0);
+    assert(sn2.get_sub().size()==2);
+
+    sn1.clear();
+    assert(sn2.is_empty());
+  }
+
+  // container node test
+  {
+    snt sn1;
+
+    snt *p1;
+    const snt *p2;
+
+    sn1.add_child(0);
+    sn1.add_child(1);
+
+    p1=sn1.add_child(2);
+    p2=p1;
+
+    assert(p1->find_leaf("a")==nullptr);
+    assert(p2->find_leaf("a")==nullptr);
+
+    p1->place_leaf("a", "b");
+    assert(p2->get_container().size()==1);
+    p1->place_leaf("c", "d");
+    assert(p2->get_container().size()==2);
+
+    assert(p2->is_container());
+
+    p1->remove_leaf("a");
+    assert(p2->get_container().size()==1);
+  }
+
+  // copy test 1
+  {
+    snt sn1;
+    snt sn2;
+
+    sn2=sn1;
+    assert(sn1.data.use_count()==3);
+    assert(sn2.data.use_count()==3);
+
+    sn1.add_child(0);
+    assert(sn1.data.use_count()==1);
+    // the newly created node is empty as well
+    assert(sn2.data.use_count()==3);
+
+    sn2=sn1;
+    assert(sn2.data.use_count()==2);
+  }
+
+  // copy test 2
+  {
+    snt sn1;
+    const snt &sn1c=sn1;
+    snt *p;
+
+    p=sn1.add_child(0);
+    p->place_leaf("x", "y");
+
+    p=sn1.add_child(1);
+    p->place_leaf("a", "b");
+    p->place_leaf("c", "d");
+
+    snt sn2;
+    const snt &sn2c=sn2;
+    sn2=sn1;
+
+    assert(sn1.is_internal());
+    assert(sn2.is_internal());
+
+    sn1.remove_child(0);
+    assert(sn1c.get_sub().size()==1);
+
+    assert(sn2c.get_sub().size()==2);
+  }
+}
+
+int main()
+{
+  sharing_node_test();  
+
+  return 0;
+}
+