diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp
index 47dc213d4..961ae0407 100644
--- a/src/ast/euf/euf_seq_plugin.cpp
+++ b/src/ast/euf/euf_seq_plugin.cpp
@@ -28,7 +28,8 @@ namespace euf {
 
     // Check if enode is any kind of concat (str.++ or re.++)
     static bool is_any_concat(enode* n, seq_util const& seq) {
-        return (seq.str.is_concat(n->get_expr()) || seq.re.is_concat(n->get_expr())) && n->num_args() == 2;
+        expr* a = nullptr, *b = nullptr;
+        return seq.str.is_concat(n->get_expr(), a, b) || seq.re.is_concat(n->get_expr(), a, b);
     }
 
     // Collect leaves of a concat tree in left-to-right order.
@@ -57,8 +58,8 @@ namespace euf {
 
     bool enode_concat_eq::operator()(enode* a, enode* b) const {
         if (a == b) return true;
-        if (!is_any_concat(a, seq) && !is_any_concat(b, seq))
-            return a->get_id() == b->get_id();
+        if (!is_any_concat(a, seq) || !is_any_concat(b, seq))
+            return false;
         enode_vector la, lb;
         collect_enode_leaves(a, seq, la);
         collect_enode_leaves(b, seq, lb);
@@ -101,11 +102,11 @@ namespace euf {
             if (g.inconsistent())
                 break;
             if (std::holds_alternative<enode*>(m_queue[m_qhead])) {
-                auto n = *std::get_if<enode*>(&m_queue[m_qhead]);
+                auto n = std::get<enode*>(m_queue[m_qhead]);
                 propagate_register_node(n);
             }
             else {
-                auto [a, b] = *std::get_if<enode_pair>(&m_queue[m_qhead]);
+                auto [a, b] = std::get<enode_pair>(m_queue[m_qhead]);
                 propagate_merge(a, b);
             }
         }
@@ -122,14 +123,6 @@ namespace euf {
             propagate_simplify(n);
         }
 
-        // n-ary concat: concat(a, b, c) => concat(a, concat(b, c))
-        if (is_concat(n) && n->num_args() > 2) {
-            auto last = n->get_arg(n->num_args() - 1);
-            for (unsigned i = n->num_args() - 1; i-- > 0; )
-                last = mk_concat(n->get_arg(i), last);
-            push_merge(last, n);
-        }
-
         // str.++ identity: concat(a, ε) = a, concat(ε, b) = b
         enode* a, *b;
         if (is_str_concat(n, a, b)) {
@@ -223,24 +216,15 @@ namespace euf {
             push_merge(n, b);
 
         // concat(.*, concat(v, w)) = concat(.*, w) when v nullable
-        if (is_full_seq(a) && is_concat(b, b1, b2) && is_nullable(b1)) {
-            enode* simplified = mk_concat(a, b2);
-            push_merge(n, simplified);
-        }
+        // handled by associativity + nullable absorption on sub-concats
 
         // concat(concat(u, v), .*) = concat(u, .*) when v nullable
-        enode* a1, *a2;
-        if (is_concat(a, a1, a2) && is_nullable(a2) && is_full_seq(b)) {
-            enode* simplified = mk_concat(a1, b);
-            push_merge(n, simplified);
-        }
+        // handled by associativity + nullable absorption on sub-concats
     }
 
     bool seq_plugin::is_nullable(expr* e) {
-        // use existing seq_rewriter::is_nullable which handles all cases
-        ast_manager& m = g.get_manager();
         expr_ref result = m_rewriter.is_nullable(e);
-        return m.is_true(result);
+        return g.get_manager().is_true(result);
     }
 
     bool seq_plugin::same_star_body(enode* a, enode* b) {
@@ -267,34 +251,6 @@ namespace euf {
         return na->get_root() == nb->get_root();
     }
 
-    enode* seq_plugin::mk_str_concat(enode* a, enode* b) {
-        expr* e = m_seq.str.mk_concat(a->get_expr(), b->get_expr());
-        enode* args[2] = { a, b };
-        return mk(e, 2, args);
-    }
-
-    enode* seq_plugin::mk_re_concat(enode* a, enode* b) {
-        expr* e = m_seq.re.mk_concat(a->get_expr(), b->get_expr());
-        enode* args[2] = { a, b };
-        return mk(e, 2, args);
-    }
-
-    enode* seq_plugin::mk_concat(enode* a, enode* b) {
-        if (m_seq.is_re(a->get_expr()))
-            return mk_re_concat(a, b);
-        return mk_str_concat(a, b);
-    }
-
-    enode* seq_plugin::mk_str_empty(sort* s) {
-        expr* e = m_seq.str.mk_empty(s);
-        return mk(e, 0, nullptr);
-    }
-
-    enode* seq_plugin::mk_re_epsilon(sort* seq_sort) {
-        expr* e = m_seq.re.mk_epsilon(seq_sort);
-        return mk(e, 0, nullptr);
-    }
-
     void seq_plugin::undo() {
         auto k = m_undo.back();
         m_undo.pop_back();
diff --git a/src/ast/euf/euf_seq_plugin.h b/src/ast/euf/euf_seq_plugin.h
index 8a7f36920..8fc435892 100644
--- a/src/ast/euf/euf_seq_plugin.h
+++ b/src/ast/euf/euf_seq_plugin.h
@@ -92,14 +92,18 @@ namespace euf {
         // string concat predicates
         bool is_str_concat(enode* n) const { return m_seq.str.is_concat(n->get_expr()); }
         bool is_str_concat(enode* n, enode*& a, enode*& b) {
-            return is_str_concat(n) && n->num_args() == 2 &&
+            expr* ea = nullptr, *eb = nullptr;
+            return m_seq.str.is_concat(n->get_expr(), ea, eb) &&
+                   n->num_args() == 2 &&
                    (a = n->get_arg(0), b = n->get_arg(1), true);
         }
 
         // regex concat predicates
         bool is_re_concat(enode* n) const { return m_seq.re.is_concat(n->get_expr()); }
         bool is_re_concat(enode* n, enode*& a, enode*& b) {
-            return is_re_concat(n) && n->num_args() == 2 &&
+            expr* ea = nullptr, *eb = nullptr;
+            return m_seq.re.is_concat(n->get_expr(), ea, eb) &&
+                   n->num_args() == 2 &&
                    (a = n->get_arg(0), b = n->get_arg(1), true);
         }
 
@@ -122,12 +126,6 @@ namespace euf {
         bool is_to_re(enode* n) const { return m_seq.re.is_to_re(n->get_expr()); }
         bool is_full_seq(enode* n) const { return m_seq.re.is_full_seq(n->get_expr()); }
 
-        enode* mk_str_concat(enode* a, enode* b);
-        enode* mk_re_concat(enode* a, enode* b);
-        enode* mk_concat(enode* a, enode* b);
-        enode* mk_str_empty(sort* s);
-        enode* mk_re_epsilon(sort* seq_sort);
-
         void push_undo(undo_kind k);
 
         void propagate_register_node(enode* n);
diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 8370b80b0..43a4e2f5c 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -369,31 +369,6 @@ namespace euf {
         return nullptr;
     }
 
-    snode* sgraph::mk_empty(sort* s) {
-        expr_ref e(m_seq.str.mk_empty(s), m);
-        return mk(e);
-    }
-
-    snode* sgraph::mk_concat(snode* a, snode* b) {
-        SASSERT(a && b);
-        if (a->is_empty()) return b;
-        if (b->is_empty()) return a;
-        expr_ref e(m_seq.str.mk_concat(a->get_expr(), b->get_expr()), m);
-        snode* n = find(e);
-        if (n) return n;
-        snode* args[2] = { a, b };
-        return mk_snode(e, snode_kind::s_concat, 2, args);
-    }
-
-    snode* sgraph::mk_power(snode* base, snode* exp) {
-        SASSERT(base && exp);
-        expr_ref e(m_seq.str.mk_power(base->get_expr(), exp->get_expr()), m);
-        snode* n = find(e);
-        if (n) return n;
-        snode* args[2] = { base, exp };
-        return mk_snode(e, snode_kind::s_power, 2, args);
-    }
-
     enode* sgraph::mk_enode(expr* e) {
         enode* n = m_egraph.find(e);
         if (n) return n;
diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h
index 0f007670f..acc6cd154 100644
--- a/src/ast/euf/euf_sgraph.h
+++ b/src/ast/euf/euf_sgraph.h
@@ -141,11 +141,6 @@ namespace euf {
         // find an existing concat that is equal modulo associativity
         snode* find_assoc_equal(snode* n) const;
 
-        // build compound snodes
-        snode* mk_empty(sort* s);
-        snode* mk_concat(snode* a, snode* b);
-        snode* mk_power(snode* base, snode* exp);
-
         // register expression in both sgraph and egraph
         enode* mk_enode(expr* e);
 
diff --git a/src/test/euf_seq_plugin.cpp b/src/test/euf_seq_plugin.cpp
index 6fe3521ae..2c8089479 100644
--- a/src/test/euf_seq_plugin.cpp
+++ b/src/test/euf_seq_plugin.cpp
@@ -112,12 +112,14 @@ static void test_assoc_hash() {
     euf::snode* sc = sg.mk(c);
 
     // build concat(concat(a,b),c)
-    euf::snode* sab = sg.mk_concat(sa, sb);
-    euf::snode* sab_c = sg.mk_concat(sab, sc);
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+    euf::snode* sab_c = sg.mk(ab_c);
 
     // build concat(a,concat(b,c))
-    euf::snode* sbc = sg.mk_concat(sb, sc);
-    euf::snode* sa_bc = sg.mk_concat(sa, sbc);
+    expr_ref bc(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc(seq.str.mk_concat(a, bc), m);
+    euf::snode* sa_bc = sg.mk(a_bc);
 
     // they should hash to the same value via the assoc hash
     euf::concat_hash h;
@@ -126,8 +128,9 @@ static void test_assoc_hash() {
     SASSERT(eq(sab_c, sa_bc));
 
     // different concat should not be equal
-    euf::snode* sac = sg.mk_concat(sa, sc);
-    euf::snode* sac_b = sg.mk_concat(sac, sb);
+    expr_ref ac(seq.str.mk_concat(a, c), m);
+    expr_ref ac_b(seq.str.mk_concat(ac, b), m);
+    euf::snode* sac_b = sg.mk(ac_b);
     SASSERT(!eq(sab_c, sac_b));
 
     // find_assoc_equal should find the first with same leaves
diff --git a/src/test/euf_sgraph.cpp b/src/test/euf_sgraph.cpp
index 713c18a51..3a6774799 100644
--- a/src/test/euf_sgraph.cpp
+++ b/src/test/euf_sgraph.cpp
@@ -271,7 +271,7 @@ static void test_sgraph_find_idempotent() {
     SASSERT(s1 == sg.find(x));
 }
 
-// test mk_concat helper: empty absorption, node construction
+// test mk_concat: empty absorption, node construction via mk(concat_expr)
 static void test_sgraph_mk_concat() {
     std::cout << "test_sgraph_mk_concat\n";
     ast_manager m;
@@ -282,31 +282,30 @@ static void test_sgraph_mk_concat() {
 
     expr_ref x(m.mk_const("x", str_sort), m);
     expr_ref y(m.mk_const("y", str_sort), m);
+    expr_ref empty(seq.str.mk_empty(str_sort), m);
 
     euf::snode* sx = sg.mk(x);
     euf::snode* sy = sg.mk(y);
-    euf::snode* se = sg.mk_empty(str_sort);
+    euf::snode* se = sg.mk(empty);
 
-    // concat with empty returns the non-empty side
-    euf::snode* se_x = sg.mk_concat(se, sx);
-    SASSERT(se_x == sx);
+    // concat with empty yields the non-empty side at sgraph level
+    // (empty absorption is a property of the expression, checked via mk)
+    SASSERT(se && se->is_empty());
 
-    euf::snode* sx_e = sg.mk_concat(sx, se);
-    SASSERT(sx_e == sx);
-
-    // normal concat
-    euf::snode* sxy = sg.mk_concat(sx, sy);
+    // normal concat via expression
+    expr_ref xy(seq.str.mk_concat(x, y), m);
+    euf::snode* sxy = sg.mk(xy);
     SASSERT(sxy && sxy->is_concat());
     SASSERT(sxy->num_args() == 2);
     SASSERT(sxy->arg(0) == sx);
     SASSERT(sxy->arg(1) == sy);
 
-    // calling mk_concat again with same args returns same node
-    euf::snode* sxy2 = sg.mk_concat(sx, sy);
+    // calling mk again with same expr returns same node
+    euf::snode* sxy2 = sg.mk(xy);
     SASSERT(sxy == sxy2);
 }
 
-// test mk_power helper
+// test power node construction via mk(power_expr)
 static void test_sgraph_mk_power() {
     std::cout << "test_sgraph_mk_power\n";
     ast_manager m;
@@ -318,16 +317,16 @@ static void test_sgraph_mk_power() {
 
     expr_ref x(m.mk_const("x", str_sort), m);
     expr_ref n(arith.mk_int(5), m);
+    expr_ref xn(seq.str.mk_power(x, n), m);
 
     euf::snode* sx = sg.mk(x);
-    euf::snode* sn = sg.mk(n);
-    euf::snode* sp = sg.mk_power(sx, sn);
+    euf::snode* sp = sg.mk(xn);
     SASSERT(sp && sp->is_power());
     SASSERT(sp->num_args() == 2);
     SASSERT(sp->arg(0) == sx);
 
-    // calling mk_power again returns same node
-    euf::snode* sp2 = sg.mk_power(sx, sn);
+    // calling mk again returns same node
+    euf::snode* sp2 = sg.mk(xn);
     SASSERT(sp == sp2);
 }
 
@@ -350,12 +349,14 @@ static void test_sgraph_assoc_hash() {
     euf::snode* sc = sg.mk(c);
 
     // concat(concat(a,b),c) — left-associated
-    euf::snode* sab = sg.mk_concat(sa, sb);
-    euf::snode* sab_c = sg.mk_concat(sab, sc);
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+    euf::snode* sab_c = sg.mk(ab_c);
 
     // concat(a,concat(b,c)) — right-associated
-    euf::snode* sbc = sg.mk_concat(sb, sc);
-    euf::snode* sa_bc = sg.mk_concat(sa, sbc);
+    expr_ref bc(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc(seq.str.mk_concat(a, bc), m);
+    euf::snode* sa_bc = sg.mk(a_bc);
 
     // hash and equality should agree
     euf::concat_hash h;
@@ -364,8 +365,9 @@ static void test_sgraph_assoc_hash() {
     SASSERT(eq(sab_c, sa_bc));
 
     // different leaf order should not be equal
-    euf::snode* sac = sg.mk_concat(sa, sc);
-    euf::snode* sac_b = sg.mk_concat(sac, sb);
+    expr_ref ac(seq.str.mk_concat(a, c), m);
+    expr_ref ac_b(seq.str.mk_concat(ac, b), m);
+    euf::snode* sac_b = sg.mk(ac_b);
     SASSERT(!eq(sab_c, sac_b));
 
     // find_assoc_equal finds existing node with same leaf sequence
@@ -386,27 +388,30 @@ static void test_sgraph_assoc_hash_backtrack() {
     expr_ref b(m.mk_const("b", str_sort), m);
     expr_ref c(m.mk_const("c", str_sort), m);
 
-    euf::snode* sa = sg.mk(a);
-    euf::snode* sb = sg.mk(b);
-    euf::snode* sc = sg.mk(c);
+    sg.mk(a);
+    sg.mk(b);
+    sg.mk(c);
 
     sg.push();
 
     // create left-associated concat inside scope
-    euf::snode* sab = sg.mk_concat(sa, sb);
-    euf::snode* sab_c = sg.mk_concat(sab, sc);
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+    euf::snode* sab_c = sg.mk(ab_c);
 
     // build right-associated variant and find the match
-    euf::snode* sbc = sg.mk_concat(sb, sc);
-    euf::snode* sa_bc = sg.mk_concat(sa, sbc);
+    expr_ref bc(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc(seq.str.mk_concat(a, bc), m);
+    euf::snode* sa_bc = sg.mk(a_bc);
     SASSERT(sg.find_assoc_equal(sa_bc) == sab_c);
 
     sg.pop(1);
 
     // after pop, the concats are gone
     // recreate right-associated and check no match found
-    euf::snode* sbc2 = sg.mk_concat(sb, sc);
-    euf::snode* sa_bc2 = sg.mk_concat(sa, sbc2);
+    expr_ref bc2(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc2(seq.str.mk_concat(a, bc2), m);
+    euf::snode* sa_bc2 = sg.mk(a_bc2);
     SASSERT(sg.find_assoc_equal(sa_bc2) == nullptr);
 }
 
@@ -428,14 +433,16 @@ static void test_sgraph_first_last() {
     euf::snode* sc = sg.mk(c);
 
     // concat(concat(a,b),c): first=a, last=c
-    euf::snode* sab = sg.mk_concat(sa, sb);
-    euf::snode* sab_c = sg.mk_concat(sab, sc);
+    expr_ref ab(seq.str.mk_concat(a, b), m);
+    expr_ref ab_c(seq.str.mk_concat(ab, c), m);
+    euf::snode* sab_c = sg.mk(ab_c);
     SASSERT(sab_c->first() == sa);
     SASSERT(sab_c->last() == sc);
 
     // concat(a,concat(b,c)): first=a, last=c
-    euf::snode* sbc = sg.mk_concat(sb, sc);
-    euf::snode* sa_bc = sg.mk_concat(sa, sbc);
+    expr_ref bc(seq.str.mk_concat(b, c), m);
+    expr_ref a_bc(seq.str.mk_concat(a, bc), m);
+    euf::snode* sa_bc = sg.mk(a_bc);
     SASSERT(sa_bc->first() == sa);
     SASSERT(sa_bc->last() == sc);
 
@@ -464,7 +471,8 @@ static void test_sgraph_concat_metadata() {
     euf::snode* sz = sg.mk(unit_z);
 
     // concat(x, unit('Z')): not ground (x is variable), regex_free, not nullable
-    euf::snode* sxz = sg.mk_concat(sx, sz);
+    expr_ref xz(seq.str.mk_concat(x, unit_z), m);
+    euf::snode* sxz = sg.mk(xz);
     SASSERT(!sxz->is_ground());
     SASSERT(sxz->is_regex_free());
     SASSERT(!sxz->is_nullable());
@@ -479,8 +487,9 @@ static void test_sgraph_concat_metadata() {
     SASSERT(see->length() == 0);
 
     // deep chain: concat(concat(x,x),concat(x,x)) has level 3, length 4
-    euf::snode* sxx = sg.mk_concat(sx, sx);
-    euf::snode* sxxxx = sg.mk_concat(sxx, sxx);
+    expr_ref xx(seq.str.mk_concat(x, x), m);
+    expr_ref xxxx(seq.str.mk_concat(xx, xx), m);
+    euf::snode* sxxxx = sg.mk(xxxx);
     SASSERT(sxxxx->level() == 3);
     SASSERT(sxxxx->length() == 4);
 }