diff --git a/src/ast/shared_occs.cpp b/src/ast/shared_occs.cpp
index 89867e8c1..9528892e7 100644
--- a/src/ast/shared_occs.cpp
+++ b/src/ast/shared_occs.cpp
@@ -21,13 +21,11 @@ Revision History:
 #include "util/ref_util.h"
 
 inline void shared_occs::insert(expr * t) {
-    obj_hashtable<expr>::entry * dummy;
-    if (m_shared.insert_if_not_there_core(t, dummy))
-        m.inc_ref(t);
+    m_shared.reserve(t->get_id() + 1);
+    m_shared[t->get_id()] = t;
 }
 
 void shared_occs::reset() { 
-    dec_ref_collection_values(m, m_shared);
     m_shared.reset(); 
 }
 
@@ -132,9 +130,15 @@ void shared_occs::operator()(expr * t) {
 }
 
 void shared_occs::display(std::ostream & out, ast_manager & m) const {
-    iterator it =  begin_shared();
-    iterator end = end_shared();
-    for (; it != end; ++it) {
-        out << mk_ismt2_pp(*it, m) << "\n";
+    for (expr* s : m_shared) {
+        if (s) {
+            out << mk_ismt2_pp(s, m) << "\n";
+        }
     }
 }
+
+unsigned shared_occs::num_shared() const{ 
+    unsigned count = 0;
+    for (expr* s : m_shared) if (s) count++;
+    return count;
+}
diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h
index 40921922a..300bb584f 100644
--- a/src/ast/shared_occs.h
+++ b/src/ast/shared_occs.h
@@ -53,7 +53,7 @@ class shared_occs {
     bool                m_track_atomic;
     bool                m_visit_quantifiers;
     bool                m_visit_patterns;
-    obj_hashtable<expr> m_shared;
+    expr_ref_vector     m_shared;
     typedef std::pair<expr*, unsigned> frame;
     svector<frame>      m_stack;
     bool process(expr * t, shared_occs_mark & visited);
@@ -64,15 +64,14 @@ public:
         m(_m),
         m_track_atomic(track_atomic),
         m_visit_quantifiers(visit_quantifiers),
-        m_visit_patterns(visit_patterns) {
+        m_visit_patterns(visit_patterns),
+        m_shared(m) {
     }
     ~shared_occs();
     void operator()(expr * t);
     void operator()(expr * t, shared_occs_mark & visited);
-    bool is_shared(expr * t) const { return m_shared.contains(t); }
-    unsigned num_shared() const { return m_shared.size(); }
-    iterator begin_shared() const { return m_shared.begin(); }
-    iterator end_shared() const { return m_shared.end(); }
+    bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; }
+    unsigned num_shared() const;
     void reset();
     void cleanup();
     void display(std::ostream & out, ast_manager & mgr) const;
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 6170a231e..7c1383d62 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -77,30 +77,12 @@ BINARY_SYM_CMD(shift_vars_cmd,
     store_expr_ref(ctx, m_sym, r.get());
 });
 
-UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
-    shared_occs s(ctx.m());
-    s(arg);
-    ctx.regular_stream() << "(shared";
-    shared_occs::iterator it  = s.begin_shared();
-    shared_occs::iterator end = s.end_shared();
-    for (; it != end; ++it) {
-        expr * curr = *it;
-        ctx.regular_stream() << std::endl << "  ";
-        ctx.display(ctx.regular_stream(), curr, 2);
-    }
-    ctx.regular_stream() << ")" << std::endl;
-});
 
 UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "assert negation", CPK_EXPR, expr *, {
     expr_ref ne(ctx.m().mk_not(arg), ctx.m());
     ctx.assert_expr(ne);
 });
 
-UNARY_CMD(num_shared_cmd, "dbg-num-shared", "<term>", "return the number of shared subterms", CPK_EXPR, expr *, {
-    shared_occs s(ctx.m());
-    s(arg);
-    ctx.regular_stream() << s.num_shared() << std::endl;
-});
 
 UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
     ctx.regular_stream() << get_num_exprs(arg) << std::endl;
@@ -550,8 +532,6 @@ void install_dbg_cmds(cmd_context & ctx) {
     ctx.insert(alloc(set_cmd));
     ctx.insert(alloc(pp_var_cmd));
     ctx.insert(alloc(shift_vars_cmd));
-    ctx.insert(alloc(pp_shared_cmd));
-    ctx.insert(alloc(num_shared_cmd));
     ctx.insert(alloc(assert_not_cmd));
     ctx.insert(alloc(size_cmd));
     ctx.insert(alloc(subst_cmd));