diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 75391812f..3dabc4a54 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -548,7 +548,7 @@ 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_dep_mgr.mk_leaf({dep_source::kind::eq, m_num_input_eqs});
+        dep_tracker dep = m_dep_mgr.mk_leaf(dep_eq{m_num_input_eqs});
         str_eq eq(lhs, rhs, dep);
         eq.sort();
         m_root->add_str_eq(eq);
@@ -558,7 +558,7 @@ 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_dep_mgr.mk_leaf({dep_source::kind::mem, m_num_input_mems});
+        dep_tracker dep = m_dep_mgr.mk_leaf(dep_mem{m_num_input_mems});
         euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
         unsigned id = next_mem_id();
         m_root->add_str_mem(str_mem(str, regex, history, id, dep));
@@ -3941,10 +3941,10 @@ namespace seq {
         vector<dep_source, false> vs;
         m_dep_mgr.linearize(deps, vs);
         for (dep_source const& d : vs) {
-            if (d.m_kind == dep_source::kind::eq)
-                eq_indices.push_back(d.index);
+            if (std::holds_alternative<dep_eq>(d))
+                eq_indices.push_back(std::get<dep_eq>(d).index);
             else
-                mem_indices.push_back(d.index);
+                mem_indices.push_back(std::get<dep_mem>(d).index);
         }
     }
 
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index faabdfb72..7406b0964 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -244,6 +244,7 @@ Author:
 #include "ast/euf/euf_sgraph.h"
 #include <functional>
 #include <map>
+#include <variant>
 #include "model/model.h"
 
 namespace seq {
@@ -303,15 +304,11 @@ namespace seq {
     };
 
     // source of a dependency: identifies an input constraint by kind and index.
-    // kind::eq means a string equality, kind::mem means a regex membership.
+    // dep_eq means a string equality, dep_mem means a regex membership.
     // index is the 0-based position in the input eq or mem list respectively.
-    struct dep_source {
-        enum class kind { eq, mem } m_kind;
-        unsigned index;
-        bool operator==(dep_source const& o) const {
-            return m_kind == o.m_kind && index == o.index;
-        }
-    };
+    struct dep_eq  { unsigned index; bool operator==(dep_eq  const& o) const { return index == o.index; } };
+    struct dep_mem { unsigned index; bool operator==(dep_mem const& o) const { return index == o.index; } };
+    using dep_source = std::variant<dep_eq, dep_mem>;
 
     // Arena-based dependency manager: builds an immutable tree of dep_source
     // leaves joined by binary join nodes.  Memory is managed via a region;
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 7cc482cfe..3eb327bb8 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -456,14 +456,15 @@ namespace smt {
         vector<seq::dep_source, false> vs;
         m_nielsen.dep_mgr().linearize(deps, vs);
         for (seq::dep_source const& d : vs) {
-            if (d.m_kind == seq::dep_source::kind::eq) {
-                eq_source const& src = m_state.get_eq_source(d.index);
+            if (std::holds_alternative<seq::dep_eq>(d)) {
+                eq_source const& src = m_state.get_eq_source(std::get<seq::dep_eq>(d).index);
                 if (src.m_n1->get_root() == src.m_n2->get_root())
                     eqs.push_back({src.m_n1, src.m_n2});
             }
             else {
-                if (d.index < m_nielsen_to_state_mem.size()) {
-                    unsigned state_mem_idx = m_nielsen_to_state_mem[d.index];
+                unsigned idx = std::get<seq::dep_mem>(d).index;
+                if (idx < m_nielsen_to_state_mem.size()) {
+                    unsigned state_mem_idx = m_nielsen_to_state_mem[idx];
                     mem_source const& src = m_state.get_mem_source(state_mem_idx);
                     SASSERT(ctx.get_assignment(src.m_lit) == l_true);
                     lits.push_back(src.m_lit);
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 4933b080d..c7bf5d429 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -45,24 +45,24 @@ static void test_dep_tracker() {
     SASSERT(d0 == nullptr);
 
     // tracker with one leaf
-    seq::dep_tracker d1 = dm.mk_leaf({seq::dep_source::kind::eq, 3});
+    seq::dep_tracker d1 = dm.mk_leaf(seq::dep_eq{3});
     SASSERT(d1 != nullptr);
 
     // tracker with another leaf
-    seq::dep_tracker d2 = dm.mk_leaf({seq::dep_source::kind::mem, 5});
+    seq::dep_tracker d2 = dm.mk_leaf(seq::dep_mem{5});
     SASSERT(d2 != nullptr);
 
     // merge
     seq::dep_tracker d3 = dm.mk_join(d1, d2);
     SASSERT(d3 != nullptr);
-    SASSERT(dm.contains(d3, {seq::dep_source::kind::eq, 3}));
-    SASSERT(dm.contains(d3, {seq::dep_source::kind::mem, 5}));
-    SASSERT(!dm.contains(d1, {seq::dep_source::kind::mem, 5}));
+    SASSERT(dm.contains(d3, seq::dep_eq{3}));
+    SASSERT(dm.contains(d3, seq::dep_mem{5}));
+    SASSERT(!dm.contains(d1, seq::dep_mem{5}));
 
     // another leaf with same value as d1
-    seq::dep_tracker d4 = dm.mk_leaf({seq::dep_source::kind::eq, 3});
-    SASSERT(dm.contains(d4, {seq::dep_source::kind::eq, 3}));
-    SASSERT(!dm.contains(d4, {seq::dep_source::kind::mem, 5}));
+    seq::dep_tracker d4 = dm.mk_leaf(seq::dep_eq{3});
+    SASSERT(dm.contains(d4, seq::dep_eq{3}));
+    SASSERT(!dm.contains(d4, seq::dep_mem{5}));
 }
 
 // test str_eq constraint creation and operations
@@ -1431,39 +1431,40 @@ static void test_dep_tracker_get_set_bits() {
     SASSERT(bits0.empty());
 
     // single leaf at eq-index 5
-    seq::dep_tracker d1 = dm.mk_leaf({seq::dep_source::kind::eq, 5});
+    seq::dep_tracker d1 = dm.mk_leaf(seq::dep_eq{5});
     vector<seq::dep_source, false> bits1;
     dm.linearize(d1, bits1);
     SASSERT(bits1.size() == 1);
-    SASSERT(bits1[0].index == 5);
-    SASSERT(bits1[0].m_kind == seq::dep_source::kind::eq);
+    SASSERT(std::get<seq::dep_eq>(bits1[0]).index == 5);
+    SASSERT(std::holds_alternative<seq::dep_eq>(bits1[0]));
 
     // two leaves merged: eq-index 3 and mem-index 11
     seq::dep_tracker d2 = dm.mk_join(
-        dm.mk_leaf({seq::dep_source::kind::eq, 3}),
-        dm.mk_leaf({seq::dep_source::kind::mem, 11}));
+        dm.mk_leaf(seq::dep_eq{3}),
+        dm.mk_leaf(seq::dep_mem{11}));
     vector<seq::dep_source, false> bits2;
     dm.linearize(d2, bits2);
     SASSERT(bits2.size() == 2);
     bool has_eq3 = false, has_mem11 = false;
     for (auto const& d : bits2) {
-        if (d.m_kind == seq::dep_source::kind::eq && d.index == 3) has_eq3 = true;
-        if (d.m_kind == seq::dep_source::kind::mem && d.index == 11) has_mem11 = true;
+        if (std::holds_alternative<seq::dep_eq>(d) && std::get<seq::dep_eq>(d).index == 3) has_eq3 = true;
+        if (std::holds_alternative<seq::dep_mem>(d) && std::get<seq::dep_mem>(d).index == 11) has_mem11 = true;
     }
     SASSERT(has_eq3);
     SASSERT(has_mem11);
 
     // join with additional leaf
     seq::dep_tracker d3 = dm.mk_join(
-        dm.mk_leaf({seq::dep_source::kind::eq, 31}),
-        dm.mk_leaf({seq::dep_source::kind::mem, 32}));
+        dm.mk_leaf(seq::dep_eq{31}),
+        dm.mk_leaf(seq::dep_mem{32}));
     vector<seq::dep_source, false> bits3;
     dm.linearize(d3, bits3);
     SASSERT(bits3.size() == 2);
     bool has31 = false, has32 = false;
     for (auto const& d : bits3) {
-        if (d.index == 31) has31 = true;
-        if (d.index == 32) has32 = true;
+        unsigned idx = std::visit([](auto const& s) { return s.index; }, d);
+        if (idx == 31) has31 = true;
+        if (idx == 32) has32 = true;
     }
     SASSERT(has31);
     SASSERT(has32);
@@ -2421,7 +2422,7 @@ static void test_length_constraints_deps() {
         ng.dep_mgr().linearize(c.m_dep, vs);
         bool found = false;
         for (auto const& d : vs)
-            if (d.m_kind == seq::dep_source::kind::eq && d.index == 0) found = true;
+            if (std::holds_alternative<seq::dep_eq>(d) && std::get<seq::dep_eq>(d).index == 0) found = true;
         SASSERT(found);
     }
 
diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp
index d8a7d0b6a..72d024d6c 100644
--- a/src/test/seq_parikh.cpp
+++ b/src/test/seq_parikh.cpp
@@ -320,7 +320,7 @@ static void test_generate_constraints_ab_star() {
     expr_ref re = mk_ab_star(m, seq);
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
-    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = dm.mk_leaf(seq::dep_mem{0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -366,7 +366,7 @@ static void test_generate_constraints_bounded_loop() {
     expr_ref re(seq.re.mk_loop(ab, 1, 3), m);
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
-    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = dm.mk_leaf(seq::dep_mem{0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -403,7 +403,7 @@ static void test_generate_constraints_stride_one() {
     expr_ref re(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
-    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = dm.mk_leaf(seq::dep_mem{0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -426,7 +426,7 @@ static void test_generate_constraints_fixed_length() {
     expr_ref re = mk_to_re_ab(m, seq);  // fixed len 2
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
-    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = dm.mk_leaf(seq::dep_mem{0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -449,7 +449,7 @@ static void test_generate_constraints_dep_propagated() {
     expr_ref re = mk_ab_star(m, seq);
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
-    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 7});
+    seq::dep_tracker dep = dm.mk_leaf(seq::dep_mem{7});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -462,7 +462,7 @@ static void test_generate_constraints_dep_propagated() {
         dm.linearize(ic.m_dep, vs);
         bool found = false;
         for (auto const& d : vs)
-            if (d.m_kind == seq::dep_source::kind::mem && d.index == 7) found = true;
+            if (std::holds_alternative<seq::dep_mem>(d) && std::get<seq::dep_mem>(d).index == 7) found = true;
         SASSERT(found);
     }
     std::cout << "  all constraints carry dep {mem,7}\n";
@@ -574,7 +574,7 @@ static void test_check_conflict_valid_k_exists() {
     ng.add_str_mem(x, regex);
 
     // lb=3, ub=5: length 4 is achievable (k=2) → no conflict
-    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf(seq::dep_mem{0});
     ng.root()->add_lower_int_bound(x, 3, dep);
     ng.root()->add_upper_int_bound(x, 5, dep);
 
@@ -602,7 +602,7 @@ static void test_check_conflict_no_valid_k() {
     ng.add_str_mem(x, regex);
 
     // lb=3, ub=3: only odd length 3 — never a multiple of 2 → conflict
-    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf(seq::dep_mem{0});
     ng.root()->add_lower_int_bound(x, 3, dep);
     ng.root()->add_upper_int_bound(x, 3, dep);
 
@@ -630,7 +630,7 @@ static void test_check_conflict_abc_star() {
     ng.add_str_mem(x, regex);
 
     // lb=5, ub=5 → no valid k (5 is not a multiple of 3) → conflict
-    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf(seq::dep_mem{0});
     ng.root()->add_lower_int_bound(x, 5, dep);
     ng.root()->add_upper_int_bound(x, 5, dep);
 
@@ -657,7 +657,7 @@ static void test_check_conflict_stride_one_never_conflicts() {
     euf::snode* regex = sg.mk(re);
     ng.add_str_mem(x, regex);
 
-    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf(seq::dep_mem{0});
     ng.root()->add_lower_int_bound(x, 7, dep);
     ng.root()->add_upper_int_bound(x, 7, dep);