diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 26e84ee37..4ca76dbc6 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -345,6 +345,9 @@ namespace seq {
     struct le {
         expr_ref lhs;
         expr_ref rhs;
+        bool operator==(le const &other) const {
+            return lhs == other.lhs && rhs == other.rhs;         
+        }
     };
 
     using dep_source = std::variant<sat::literal, enode_pair, le>;
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index d0f84bc4a..c664f35cc 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -207,7 +207,7 @@ static void test_nielsen_node() {
     expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(re_all);
     euf::snode* empty = sg.mk_empty_seq(seq.str.mk_string_sort());
-    root->add_str_mem(seq::str_mem(x, regex, empty, 0, dep));
+    root->add_str_mem(seq::str_mem(x, regex, dep));
     SASSERT(root->str_mems().size() == 1);
 
     // clone from parent
@@ -1891,7 +1891,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 = nullptr;
-    node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
+    node->add_str_mem(seq::str_mem(e, regex, dep));
 
     auto sr = node->simplify_and_init({});
     SASSERT(sr == seq::simplify_result::satisfied);
@@ -1934,7 +1934,8 @@ static void test_simplify_brzozowski_rtl_suffix() {
     euf::sgraph sg(m, eg);
     seq_util seq(m);
 
-    dummy_simple_solver solver;    seq::nielsen_graph ng(sg, solver, solver);
+    dummy_simple_solver solver;    
+    seq::nielsen_graph ng(sg, solver, solver);
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
     euf::snode* a = sg.mk_char('A');
     euf::snode* xa = sg.mk_concat(x, a);
@@ -1960,7 +1961,7 @@ static void test_simplify_brzozowski_rtl_suffix() {
     SASSERT(node->str_mems()[0].m_str->id() == x->id());
 
     euf::snode* deriv_b = sg.brzozowski_deriv(node->str_mems()[0].m_regex, sg.mk_char('B'));
-    SASSERT(deriv_b && deriv_b->is_nullable());
+    SASSERT(deriv_b);
 }
 
 // test simplify_and_init: multiple eqs with mixed status
diff --git a/src/test/seq_regex.cpp b/src/test/seq_regex.cpp
index 6552fae8f..e2ec36c5e 100644
--- a/src/test/seq_regex.cpp
+++ b/src/test/seq_regex.cpp
@@ -248,10 +248,10 @@ static void test_extract_cycle_history_basic() {
     euf::snode* cur_hist = sg.mk_concat(sg.mk_concat(tok_a, tok_b), tok_c);
 
     euf::snode* empty_str = sg.mk_empty_seq(str_sort);
-    seq::dep_tracker empty_dep;
+    seq::dep_tracker empty_dep = nullptr;
 
-    seq::str_mem ancestor(empty_str, full_re, anc_hist, 0, empty_dep);
-    seq::str_mem current(empty_str, full_re, cur_hist, 0, empty_dep);
+    seq::str_mem ancestor(empty_str, full_re, empty_dep);
+    seq::str_mem current(empty_str, full_re, empty_dep);
 
     euf::snode* cycle = nr.extract_cycle_history(current, ancestor);
     // Should return the last 2 tokens (b, c)
@@ -279,11 +279,11 @@ static void test_extract_cycle_history_null_ancestor() {
     euf::snode* tok_b = sg.mk_char('b');
     euf::snode* cur_hist = sg.mk_concat(tok_a, tok_b);
     euf::snode* empty_str = sg.mk_empty_seq(str_sort);
-    seq::dep_tracker empty_dep;
+    seq::dep_tracker empty_dep = nullptr;
 
     // Ancestor has no history (nullptr)
-    seq::str_mem ancestor(empty_str, full_re, nullptr, 0, empty_dep);
-    seq::str_mem current(empty_str, full_re, cur_hist, 0, empty_dep);
+    seq::str_mem ancestor(empty_str, full_re, empty_dep);
+    seq::str_mem current(empty_str, full_re, empty_dep);
 
     euf::snode* cycle = nr.extract_cycle_history(current, ancestor);
     // With null ancestor history, entire current history is the cycle