diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 6e8827a79..329326de9 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -450,8 +450,8 @@ namespace euf {
         m_egraph.pop(num_scopes);
     }
 
-    snode* sgraph::mk_var(symbol const& name) {
-        expr_ref e(m.mk_const(name, m_str_sort), m);
+    snode* sgraph::mk_var(symbol const& name, sort* s) {
+        expr_ref e(m.mk_const(name, s), m);
         return mk(e);
     }
 
diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h
index 545f21c38..9029235bc 100644
--- a/src/ast/euf/euf_sgraph.h
+++ b/src/ast/euf/euf_sgraph.h
@@ -126,7 +126,7 @@ namespace euf {
         enode* mk_enode(expr* e);
 
         // factory methods for creating snodes with corresponding expressions
-        snode* mk_var(symbol const& name);
+        snode* mk_var(symbol const& name, sort* s);
         snode* mk_char(unsigned ch);
         snode* mk_empty();
         snode* mk_concat(snode* a, snode* b);
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index 95bf1f64e..37b8a02d6 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -98,6 +98,7 @@ namespace euf {
 
     public:
         expr*      get_expr() const { return m_expr; }
+        sort*      get_sort() const { SASSERT(m_expr); return m_expr->get_sort(); }
         snode_kind kind()     const { return m_kind; }
         unsigned   id()       const { return m_id; }
         unsigned   num_args() const { return m_num_args; }
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 6decb616d..195b2fa67 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1225,7 +1225,7 @@ namespace seq {
                 }
                 // branch 2: y → char·fresh (progress)
                 {
-                    euf::snode* fresh = mk_fresh_var();
+                    euf::snode* fresh = mk_fresh_var(rhead->get_sort());
                     euf::snode* replacement = m_sg.mk_concat(lhead, fresh);
                     nielsen_node* child = mk_child(node);
                     nielsen_edge* e = mk_edge(node, child, true);
@@ -1248,7 +1248,7 @@ namespace seq {
                 }
                 // branch 2: x → char·fresh (progress)
                 {
-                    euf::snode* fresh = mk_fresh_var();
+                    euf::snode* fresh = mk_fresh_var(lhead->get_sort());
                     euf::snode* replacement = m_sg.mk_concat(rhead, fresh);
                     nielsen_node* child = mk_child(node);
                     nielsen_edge* e = mk_edge(node, child, true);
@@ -1294,7 +1294,7 @@ namespace seq {
             }
             // child 2: x → y·x' (progress)
             {
-                euf::snode* fresh = mk_fresh_var();
+                euf::snode* fresh = mk_fresh_var(lhead->get_sort());
                 euf::snode* replacement = m_sg.mk_concat(rhead, fresh);
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, true);
@@ -1304,7 +1304,7 @@ namespace seq {
             }
             // child 3: y → x·y' (progress)
             {
-                euf::snode* fresh = mk_fresh_var();
+                euf::snode* fresh = mk_fresh_var(rhead->get_sort());
                 euf::snode* replacement = m_sg.mk_concat(lhead, fresh);
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, true);
@@ -1534,7 +1534,7 @@ namespace seq {
 
             euf::snode* pad = nullptr;
             if (padding != 0) {
-                pad = mk_fresh_var();
+                pad = mk_fresh_var(lhs_toks[0]->get_sort());
                 if (padding > 0) {
                     // LHS prefix is longer by |padding| constants.
                     // Prepend pad to RHS prefix, append pad to LHS suffix.
@@ -1585,10 +1585,10 @@ namespace seq {
     // nielsen_graph: mk_fresh_var
     // -----------------------------------------------------------------------
 
-    euf::snode* nielsen_graph::mk_fresh_var() {
+    euf::snode* nielsen_graph::mk_fresh_var(sort* s) {
         ++m_stats.m_num_fresh_vars;
         std::string name = "v!" + std::to_string(m_fresh_cnt++);
-        return m_sg.mk_var(symbol(name.c_str()));
+        return m_sg.mk_var(symbol(name.c_str()), s);
     }
 
     euf::snode* nielsen_graph::mk_fresh_char_var() {
@@ -1705,7 +1705,7 @@ namespace seq {
                 if (!deriv || deriv->is_fail())
                     continue;
 
-                euf::snode* fresh = mk_fresh_var();
+                euf::snode* fresh = mk_fresh_var(first->get_sort());
                 euf::snode* replacement = m_sg.mk_concat(ch, fresh);
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, true);
@@ -2001,7 +2001,7 @@ namespace seq {
         // Side constraint: n >= 1
         // Use fresh power variable for u^(n-1)
         {
-            euf::snode* fresh_power = mk_fresh_var();
+            euf::snode* fresh_power = mk_fresh_var(base->get_sort());
             euf::snode* replacement = m_sg.mk_concat(base, fresh_power);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, false);
@@ -2040,8 +2040,8 @@ namespace seq {
             // replacing x → z·fresh_post. This breaks the cycle because
             // z is a new variable that won't trigger star_intr again.
             euf::snode* x = first;
-            euf::snode* z = mk_fresh_var();
-            euf::snode* fresh_post = mk_fresh_var();
+            euf::snode* z = mk_fresh_var(x->get_sort());
+            euf::snode* fresh_post = mk_fresh_var(x->get_sort());
             euf::snode* str_tail = m_sg.drop_first(mem.m_str);
 
             // Build z ∈ R* membership: the star of the current regex
@@ -2234,7 +2234,7 @@ namespace seq {
                 euf::snode* deriv = m_sg.brzozowski_deriv(mem.m_regex, mt);
                 if (deriv && deriv->is_fail()) continue;
 
-                euf::snode* fresh_var = mk_fresh_var();
+                euf::snode* fresh_var = mk_fresh_var(first->get_sort());
                 euf::snode* fresh_char = mk_fresh_char_var();
                 euf::snode* replacement = m_sg.mk_concat(fresh_char, fresh_var);
                 nielsen_node* child = mk_child(node);
@@ -2282,8 +2282,8 @@ namespace seq {
         // Side constraints: m >= 0, m < n (i.e., n >= m + 1)
         {
             expr_ref fresh_m = mk_fresh_int_var();
-            euf::snode* fresh_power = mk_fresh_var(); // represents base^m
-            euf::snode* fresh_suffix = mk_fresh_var(); // represents prefix(base)
+            euf::snode* fresh_power = mk_fresh_var(base->get_sort()); // represents base^m
+            euf::snode* fresh_suffix = mk_fresh_var(base->get_sort()); // represents prefix(base)
             euf::snode* replacement = m_sg.mk_concat(fresh_power, fresh_suffix);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, true);
@@ -2302,7 +2302,7 @@ namespace seq {
         // Branch 2: x = u^n · x' (variable extends past full power, non-progress)
         // Side constraint: n >= 0
         {
-            euf::snode* fresh_tail = mk_fresh_var();
+            euf::snode* fresh_tail = mk_fresh_var(base->get_sort());
             // Peel one base unit (approximation of extending past the power)
             euf::snode* replacement = m_sg.mk_concat(base, fresh_tail);
             nielsen_node* child = mk_child(node);
@@ -2357,7 +2357,7 @@ namespace seq {
         // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1)
         // Side constraint: n >= 1
         {
-            euf::snode* fresh = mk_fresh_var();
+            euf::snode* fresh = mk_fresh_var(base->get_sort());
             euf::snode* replacement = m_sg.mk_concat(base, fresh);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, false);
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 7b571b108..8af96d962 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -761,7 +761,7 @@ namespace seq {
         search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
 
         // create a fresh variable with a unique name
-        euf::snode* mk_fresh_var();
+        euf::snode* mk_fresh_var(sort* s);
 
         // create a fresh symbolic character: seq.unit(fresh_char_const)
         // analogous to ZIPT's SymCharToken creation