diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 2eb0e740b..3650cdcb1 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -1529,177 +1529,6 @@ static void test_solve_eval_idx_tracking() {
     SASSERT(root->eval_idx() == ng.run_idx());
 }
 
-// test is_subsumed_by: node with superset of constraints is subsumed
-static void test_is_subsumed_by_basic() {
-    std::cout << "test_is_subsumed_by_basic\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* y = sg.mk_var(symbol("y"));
-    euf::snode* z = sg.mk_var(symbol("z"));
-
-    seq::dep_tracker dep(4, 0);
-
-    // node1 has {x=y, x=z}
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-    n1->add_str_eq(seq::str_eq(x, z, dep));
-
-    // node2 has {x=y} (subset of node1)
-    seq::nielsen_node* n2 = ng.mk_node();
-    n2->add_str_eq(seq::str_eq(x, y, dep));
-
-    // n1 is subsumed by n2 (n2's constraints are a subset of n1's)
-    SASSERT(n1->is_subsumed_by(*n2));
-    // n2 is NOT subsumed by n1 (n1 has x=z which n2 doesn't)
-    SASSERT(!n2->is_subsumed_by(*n1));
-}
-
-// test is_subsumed_by: trivial equations are skipped
-static void test_is_subsumed_by_trivial_skip() {
-    std::cout << "test_is_subsumed_by_trivial_skip\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* y = sg.mk_var(symbol("y"));
-    euf::snode* e = sg.mk_empty();
-
-    seq::dep_tracker dep(4, 0);
-
-    // node1 has {x=y}
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-
-    // node2 has {x=y, ε=ε} (extra trivial eq)
-    seq::nielsen_node* n2 = ng.mk_node();
-    n2->add_str_eq(seq::str_eq(x, y, dep));
-    n2->add_str_eq(seq::str_eq(e, e, dep));
-
-    // n1 is subsumed by n2 (n2's non-trivial constraints ⊆ n1's)
-    SASSERT(n1->is_subsumed_by(*n2));
-    // n2 is also subsumed by n1 (n1's constraints ⊆ n2's)
-    SASSERT(n2->is_subsumed_by(*n1));
-}
-
-// test is_subsumed_by: non-matching constraints
-static void test_is_subsumed_by_no_match() {
-    std::cout << "test_is_subsumed_by_no_match\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* y = sg.mk_var(symbol("y"));
-    euf::snode* z = sg.mk_var(symbol("z"));
-
-    seq::dep_tracker dep(4, 0);
-
-    // node1 has {x=y}
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-
-    // node2 has {x=z} (different constraint)
-    seq::nielsen_node* n2 = ng.mk_node();
-    n2->add_str_eq(seq::str_eq(x, z, dep));
-
-    SASSERT(!n1->is_subsumed_by(*n2));
-    SASSERT(!n2->is_subsumed_by(*n1));
-}
-
-// test is_subsumed_by: identical constraint sets
-static void test_is_subsumed_by_exact_match() {
-    std::cout << "test_is_subsumed_by_exact_match\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* y = sg.mk_var(symbol("y"));
-
-    seq::dep_tracker dep(4, 0);
-
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-
-    seq::nielsen_node* n2 = ng.mk_node();
-    n2->add_str_eq(seq::str_eq(x, y, dep));
-
-    // identical sets: mutual subsumption
-    SASSERT(n1->is_subsumed_by(*n2));
-    SASSERT(n2->is_subsumed_by(*n1));
-}
-
-// test is_subsumed_by with str_mem constraints
-static void test_is_subsumed_by_str_mem() {
-    std::cout << "test_is_subsumed_by_str_mem\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-    seq_util seq(m);
-    sort_ref str_sort(seq.str.mk_string_sort(), m);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* e = sg.mk_empty();
-
-    expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
-    euf::snode* regex = sg.mk(re_all);
-
-    seq::dep_tracker dep(4, 0);
-
-    // node1 has {x ∈ re_all, x=x_eq}
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_mem(seq::str_mem(x, regex, e, 0, dep));
-    euf::snode* y = sg.mk_var(symbol("y"));
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-
-    // node2 has {x ∈ re_all} only (subset)
-    seq::nielsen_node* n2 = ng.mk_node();
-    n2->add_str_mem(seq::str_mem(x, regex, e, 0, dep));
-
-    SASSERT(n1->is_subsumed_by(*n2));
-    SASSERT(!n2->is_subsumed_by(*n1));
-}
-
-// test is_subsumed_by: empty node subsumes everything
-static void test_is_subsumed_by_empty() {
-    std::cout << "test_is_subsumed_by_empty\n";
-    ast_manager m;
-    reg_decl_plugins(m);
-    euf::egraph eg(m);
-    euf::sgraph sg(m, eg);
-
-    seq::nielsen_graph ng(sg);
-    euf::snode* x = sg.mk_var(symbol("x"));
-    euf::snode* y = sg.mk_var(symbol("y"));
-
-    seq::dep_tracker dep(4, 0);
-
-    // node1 has {x=y}
-    seq::nielsen_node* n1 = ng.mk_node();
-    n1->add_str_eq(seq::str_eq(x, y, dep));
-
-    // node2 is empty
-    seq::nielsen_node* n2 = ng.mk_node();
-
-    // n1 is subsumed by empty n2 (empty set is subset of everything)
-    SASSERT(n1->is_subsumed_by(*n2));
-    // n2 is NOT subsumed by n1 (n1 has x=y which n2 doesn't)
-    SASSERT(!n2->is_subsumed_by(*n1));
-}
 
 // -----------------------------------------------------------------------
 // Direct simplify_and_init tests
@@ -3332,12 +3161,6 @@ void tst_seq_nielsen() {
     test_solve_mixed_eq_mem_sat();
     test_solve_children_failed_reason();
     test_solve_eval_idx_tracking();
-    test_is_subsumed_by_basic();
-    test_is_subsumed_by_trivial_skip();
-    test_is_subsumed_by_no_match();
-    test_is_subsumed_by_exact_match();
-    test_is_subsumed_by_str_mem();
-    test_is_subsumed_by_empty();
     test_simplify_prefix_cancel();
     test_simplify_symbol_clash();
     test_simplify_empty_propagation();