diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 33e06e293..ed073bf0c 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -4125,11 +4125,6 @@ namespace seq {
         return exp_snode ? exp_snode->get_expr() : nullptr;
     }
 
-    expr_ref nielsen_graph::mk_fresh_int_var() {
-        std::string name = "n!" + std::to_string(m_fresh_cnt++);
-        return expr_ref(m.mk_fresh_const(name.c_str(), a.mk_int()), m);
-    }
-
     // -----------------------------------------------------------------------
     // Regex widening: overapproximate string and check intersection emptiness
     // Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380)
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index fe387e1b2..e14ab1960 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -1141,9 +1141,6 @@ namespace seq {
         // get the exponent expression from a power snode (arg(1))
         expr* get_power_exponent(euf::snode* power);
 
-        // create a fresh integer variable expression (for power exponents)
-        expr_ref mk_fresh_int_var();
-
         // -----------------------------------------------
         // Modification counter methods for substitution length tracking.
         // mirrors ZIPT's NielsenEdge.IncModCount / DecModCount and