diff --git a/src/ast/rewriter/seq_regex_bisim.cpp b/src/ast/rewriter/seq_regex_bisim.cpp
index 833c36dca..f21b3fb54 100644
--- a/src/ast/rewriter/seq_regex_bisim.cpp
+++ b/src/ast/rewriter/seq_regex_bisim.cpp
@@ -34,7 +34,6 @@ namespace seq {
 
     void regex_bisim::reset() {
         m_uf.reset();
-        m_node_of.reset();
         m_pinned.reset();
         m_worklist.reset();
         m_steps = 0;
@@ -45,13 +44,10 @@ namespace seq {
        first encounter.
     */
     unsigned regex_bisim::node_of(expr* r) {
-        unsigned id = 0;
-        if (m_node_of.find(r, id))
-            return id;
-        id = m_uf.mk_var();
-        m_node_of.insert(r, id);
+        while (r->get_id() >= m_uf.get_num_vars())
+            m_uf.mk_var();
         m_pinned.push_back(r);
-        return id;
+        return r->get_id();
     }
 
     /*
diff --git a/src/ast/rewriter/seq_regex_bisim.h b/src/ast/rewriter/seq_regex_bisim.h
index 561088270..2f6a54805 100644
--- a/src/ast/rewriter/seq_regex_bisim.h
+++ b/src/ast/rewriter/seq_regex_bisim.h
@@ -65,7 +65,6 @@ namespace seq {
         seq_rewriter&            m_rw;
         seq_util                 m_util;
         basic_union_find         m_uf;
-        obj_map<expr, unsigned>  m_node_of;
         expr_ref_vector          m_pinned;
         expr_ref_vector          m_worklist;
         unsigned                 m_step_bound { 50000 };