diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 85bf09f08..37f7c3556 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -23,7 +23,6 @@ Author:
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "math/lp/lar_solver.h"
-#include "util/bit_util.h"
 #include "util/hashtable.h"
 #include <algorithm>
 #include <cstdlib>
@@ -31,58 +30,6 @@ Author:
 
 namespace seq {
 
-    // -----------------------------------------------
-    // dep_tracker
-    // -----------------------------------------------
-
-    dep_tracker::dep_tracker(unsigned num_bits) {
-        unsigned words = (num_bits + 31) / 32;
-        m_bits.resize(words, 0);
-    }
-
-    dep_tracker::dep_tracker(unsigned num_bits, unsigned set_bit) : dep_tracker(num_bits) {
-        if (set_bit < num_bits) {
-            unsigned word_idx = set_bit / 32;
-            unsigned bit_idx = set_bit % 32;
-            m_bits[word_idx] = 1u << bit_idx;
-        }
-    }
-
-    void dep_tracker::merge(dep_tracker const& other) {
-        if (other.m_bits.empty())
-            return;
-        if (m_bits.size() < other.m_bits.size())
-            m_bits.resize(other.m_bits.size(), 0);
-        for (unsigned i = 0; i < other.m_bits.size(); ++i)
-            m_bits[i] |= other.m_bits[i];
-    }
-
-    bool dep_tracker::is_superset(dep_tracker const& other) const {
-        for (unsigned i = 0; i < other.m_bits.size(); ++i) {
-            unsigned my_bits = (i < m_bits.size()) ? m_bits[i] : 0;
-            if ((my_bits & other.m_bits[i]) != other.m_bits[i])
-                return false;
-        }
-        return true;
-    }
-
-    bool dep_tracker::empty() const {
-        for (unsigned b : m_bits)
-            if (b != 0) return false;
-        return true;
-    }
-
-    void dep_tracker::get_set_bits(unsigned_vector& indices) const {
-        for (unsigned i = 0; i < m_bits.size(); ++i) {
-            unsigned word = m_bits[i];
-            while (word != 0) {
-                unsigned bit = i * 32 + ntz_core(word);
-                indices.push_back(bit);
-                word &= word - 1; // clear lowest set bit
-            }
-        }
-    }
-
     // -----------------------------------------------
     // str_eq
     // -----------------------------------------------
@@ -338,7 +285,7 @@ namespace seq {
             str_eq& eq = m_str_eq[i];
             eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement);
             eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement);
-            eq.m_dep.merge(s.m_dep);
+            eq.m_dep |= s.m_dep;
             eq.sort();
         }
         for (unsigned i = 0; i < m_str_mem.size(); ++i) {
@@ -346,7 +293,7 @@ namespace seq {
             mem.m_str = sg.subst(mem.m_str, s.m_var, s.m_replacement);
             // regex is typically ground, but apply subst for generality
             mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement);
-            mem.m_dep.merge(s.m_dep);
+            mem.m_dep |= s.m_dep;
         }
     }
 
@@ -469,8 +416,8 @@ namespace seq {
     void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
         if (!m_root)
             m_root = mk_node();
-        dep_tracker dep(m_root->str_eqs().size() + m_root->str_mems().size() + 1,
-                        m_root->str_eqs().size());
+        dep_tracker dep;
+        dep.insert(m_root->str_eqs().size());
         str_eq eq(lhs, rhs, dep);
         eq.sort();
         m_root->add_str_eq(eq);
@@ -480,8 +427,8 @@ namespace seq {
     void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) {
         if (!m_root)
             m_root = mk_node();
-        dep_tracker dep(m_root->str_eqs().size() + m_root->str_mems().size() + 1,
-                        m_root->str_eqs().size() + m_root->str_mems().size());
+        dep_tracker dep;
+        dep.insert(m_root->str_eqs().size() + m_root->str_mems().size());
         euf::snode* history = m_sg.mk_empty();
         unsigned id = next_mem_id();
         m_root->add_str_mem(str_mem(str, regex, history, id, dep));
@@ -2389,9 +2336,9 @@ namespace seq {
             if (!n->is_currently_conflict())
                 continue;
             for (str_eq const& eq : n->str_eqs())
-                deps.merge(eq.m_dep);
+                deps |= eq.m_dep;
             for (str_mem const& mem : n->str_mems())
-                deps.merge(mem.m_dep);
+                deps |= mem.m_dep;
         }
     }
 
@@ -2399,9 +2346,7 @@ namespace seq {
         SASSERT(m_root);
         dep_tracker deps;
         collect_conflict_deps(deps);
-        unsigned_vector bits;
-        deps.get_set_bits(bits);
-        for (unsigned b : bits) {
+        for (unsigned b : deps) {
             if (b < m_num_input_eqs)
                 eq_indices.push_back(b);
             else
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 47e74bdc7..f507aa9b8 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -98,10 +98,8 @@ Abstract:
     ------------------------------------
     1. dep_tracker (DependencyTracker): ZIPT's DependencyTracker is a .NET
        class using a BitArray-like structure for tracking constraint origins.
-       Z3's dep_tracker uses a dense bitvector stored as svector<unsigned>
-       (32-bit words). The merge/is_superset/empty semantics are equivalent,
-       but the representation is more cache-friendly and avoids managed-heap
-       allocation.
+       Z3 uses uint_set (a dense bitvector from util/uint_set.h) for the same
+       purpose. The |=/subset_of/empty semantics are equivalent.
 
     2. Substitution application (nielsen_node::apply_subst): ZIPT uses an
        immutable, functional style -- Apply() returns a new constraint if
@@ -276,23 +274,7 @@ namespace seq {
     // dependency tracker: bitvector tracking which input constraints
     // contributed to deriving a given constraint
     // mirrors ZIPT's DependencyTracker
-    class dep_tracker {
-        svector<unsigned> m_bits;
-    public:
-        dep_tracker() = default;
-        explicit dep_tracker(unsigned num_bits);
-        dep_tracker(unsigned num_bits, unsigned set_bit);
-
-        void merge(dep_tracker const& other);
-        bool is_superset(dep_tracker const& other) const;
-        bool empty() const;
-
-        // collect indices of all set bits into 'indices'
-        void get_set_bits(unsigned_vector& indices) const;
-
-        bool operator==(dep_tracker const& other) const { return m_bits == other.m_bits; }
-        bool operator!=(dep_tracker const& other) const { return !(*this == other); }
-    };
+    using dep_tracker = uint_set;
 
     // -----------------------------------------------
     // character range and set types
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index e231ea82a..5e11fe7cf 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -450,10 +450,8 @@ namespace smt {
 
     void theory_nseq::deps_to_lits(seq::dep_tracker const& deps, enode_pair_vector& eqs, literal_vector& lits) {
         context& ctx = get_context();
-        unsigned_vector bits;
-        deps.get_set_bits(bits);
         unsigned num_input_eqs = m_nielsen.num_input_eqs();
-        for (unsigned b : bits) {
+        for (unsigned b : deps) {
             if (b < num_input_eqs) {
                 eq_source const& src = m_state.get_eq_source(b);
                 if (src.m_n1->get_root() == src.m_n2->get_root())
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 1a6321ab2..92d5bb72e 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -22,7 +22,7 @@ Abstract:
 #include "ast/ast_pp.h"
 #include <iostream>
 
-// test dep_tracker basic operations
+// test dep_tracker (uint_set) basic operations
 static void test_dep_tracker() {
     std::cout << "test_dep_tracker\n";
 
@@ -31,23 +31,26 @@ static void test_dep_tracker() {
     SASSERT(d0.empty());
 
     // tracker with one bit set
-    seq::dep_tracker d1(8, 3);
+    seq::dep_tracker d1;
+    d1.insert(3);
     SASSERT(!d1.empty());
 
     // tracker with another bit
-    seq::dep_tracker d2(8, 5);
+    seq::dep_tracker d2;
+    d2.insert(5);
     SASSERT(!d2.empty());
 
     // merge
     seq::dep_tracker d3 = d1;
-    d3.merge(d2);
+    d3 |= d2;
     SASSERT(!d3.empty());
-    SASSERT(d3.is_superset(d1));
-    SASSERT(d3.is_superset(d2));
-    SASSERT(!d1.is_superset(d2));
+    SASSERT(d1.subset_of(d3));
+    SASSERT(d2.subset_of(d3));
+    SASSERT(!d2.subset_of(d1));
 
     // equality
-    seq::dep_tracker d4(8, 3);
+    seq::dep_tracker d4;
+    d4.insert(3);
     SASSERT(d1 == d4);
     SASSERT(d1 != d2);
 }
@@ -65,7 +68,7 @@ static void test_str_eq() {
     euf::snode* a = sg.mk_char('A');
     euf::snode* e = sg.mk_empty();
 
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
 
     // basic equality
     seq::str_eq eq1(x, y, dep);
@@ -112,7 +115,7 @@ static void test_str_mem() {
     expr_ref star_fc(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(star_fc);
 
-    seq::dep_tracker dep(4, 1);
+    seq::dep_tracker dep; dep.insert(1);
     seq::str_mem mem(x, regex, e, 0, dep);
 
     // x in regex is primitive (x is a single variable)
@@ -1322,37 +1325,40 @@ static void test_solve_conflict_deps() {
     SASSERT(!deps.empty());
 }
 
-// test dep_tracker::get_set_bits
+// test dep_tracker (uint_set) iteration
 static void test_dep_tracker_get_set_bits() {
     std::cout << "test_dep_tracker_get_set_bits\n";
 
     // empty tracker has no bits
     seq::dep_tracker d0;
     unsigned_vector bits0;
-    d0.get_set_bits(bits0);
+    for (unsigned b : d0) bits0.push_back(b);
     SASSERT(bits0.empty());
 
     // single bit set at position 5
-    seq::dep_tracker d1(16, 5);
+    seq::dep_tracker d1;
+    d1.insert(5);
     unsigned_vector bits1;
-    d1.get_set_bits(bits1);
+    for (unsigned b : d1) bits1.push_back(b);
     SASSERT(bits1.size() == 1);
     SASSERT(bits1[0] == 5);
 
     // two bits merged
-    seq::dep_tracker d2(16, 3);
-    d2.merge(seq::dep_tracker(16, 11));
+    seq::dep_tracker d2;
+    d2.insert(3);
+    d2.insert(11);
     unsigned_vector bits2;
-    d2.get_set_bits(bits2);
+    for (unsigned b : d2) bits2.push_back(b);
     SASSERT(bits2.size() == 2);
     SASSERT(bits2[0] == 3);
     SASSERT(bits2[1] == 11);
 
     // test across word boundary (bit 31 and 32)
-    seq::dep_tracker d3(64, 31);
-    d3.merge(seq::dep_tracker(64, 32));
+    seq::dep_tracker d3;
+    d3.insert(31);
+    d3.insert(32);
     unsigned_vector bits3;
-    d3.get_set_bits(bits3);
+    for (unsigned b : d3) bits3.push_back(b);
     SASSERT(bits3.size() == 2);
     SASSERT(bits3[0] == 31);
     SASSERT(bits3[1] == 32);
@@ -1543,7 +1549,7 @@ static void test_simplify_prefix_cancel() {
     euf::snode* aby = sg.mk_concat(a, sg.mk_concat(b, y));
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(abx, aby, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1573,7 +1579,7 @@ static void test_simplify_symbol_clash() {
     euf::snode* by = sg.mk_concat(b, y);
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(ax, by, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1598,7 +1604,7 @@ static void test_simplify_empty_propagation() {
 
     // ε = x·y → forces x=ε, y=ε → all trivial → satisfied
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(e, xy, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1619,7 +1625,7 @@ static void test_simplify_empty_vs_char() {
 
     // ε = A → rhs has non-variable token → conflict
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(e, a, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1645,7 +1651,7 @@ static void test_simplify_multi_pass_clash() {
     euf::snode* ac = sg.mk_concat(a, c);
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(ab, ac, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1667,7 +1673,7 @@ static void test_simplify_trivial_removal() {
     euf::snode* e = sg.mk_empty();
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(e, e, dep));  // trivial
     node->add_str_eq(seq::str_eq(x, y, dep));  // non-trivial
 
@@ -1689,7 +1695,7 @@ static void test_simplify_all_trivial_satisfied() {
     euf::snode* e = sg.mk_empty();
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_eq(seq::str_eq(x, x, dep));  // trivial: same pointer
     node->add_str_eq(seq::str_eq(e, e, dep));  // trivial: both empty
 
@@ -1716,7 +1722,7 @@ static void test_simplify_regex_infeasible() {
 
     // ε ∈ to_re("A") → non-nullable → conflict
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1744,7 +1750,7 @@ static void test_simplify_nullable_removal() {
 
     // ε ∈ star(to_re("A")) → nullable → satisfied, mem removed
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1772,7 +1778,7 @@ static void test_simplify_brzozowski_sat() {
 
     // "A" ∈ to_re("A") → derivative consumes 'A' → ε ∈ ε-regex → satisfied
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(4, 0);
+    seq::dep_tracker dep; dep.insert(0);
     node->add_str_mem(seq::str_mem(a, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init(ng);
@@ -1795,7 +1801,7 @@ static void test_simplify_multiple_eqs() {
     euf::snode* e = sg.mk_empty();
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep(8, 0);
+    seq::dep_tracker dep; dep.insert(0);
 
     // eq1: ε = ε (trivial → removed)
     node->add_str_eq(seq::str_eq(e, e, dep));
@@ -2234,7 +2240,7 @@ static void test_length_constraints_deps() {
     for (auto const& c : constraints) {
         SASSERT(!c.m_dep.empty());
         unsigned_vector bits;
-        c.m_dep.get_set_bits(bits);
+        for (unsigned b : c.m_dep) bits.push_back(b);
         SASSERT(bits.size() == 1);
         SASSERT(bits[0] == 0);
     }