diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 4447eeac4..629179ab3 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -241,11 +241,7 @@ namespace seq {
     // nielsen_graph
     // -----------------------------------------------
 
-    nielsen_graph::nielsen_graph(euf::sgraph& sg):
-        m_sg(sg) {
-    }
-
-    nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver* solver):
+    nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver):
         m_sg(sg),
         m_solver(solver) {
     }
@@ -2394,20 +2390,13 @@ namespace seq {
         if (constraints.empty())
             return true; // no integer constraints, trivially feasible
 
-        if (!m_solver) {
-            // No solver provided: skip arithmetic feasibility checking.
-            // This makes the Nielsen graph unsound with respect to integer constraints
-            // but is acceptable for contexts (e.g., unit tests) that only exercise
-            // string equality patterns without arithmetic path constraints.
-            return true;
-        }
 
-        m_solver->push();
+        m_solver.push();
         for (auto const& ic : constraints)
-            m_solver->assert_expr(int_constraint_to_expr(ic));
+            m_solver.assert_expr(int_constraint_to_expr(ic));
 
-        lbool result = m_solver->check();
-        m_solver->pop(1);
+        lbool result = m_solver.check();
+        m_solver.pop(1);
         return result != l_false;
     }
 
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index fb8cc0096..5b9cfcd89 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -660,15 +660,12 @@ namespace seq {
         // When m_solver is null, check_int_feasibility skips arithmetic checking
         // and optimistically assumes feasibility.
         // -----------------------------------------------
-        simple_solver*                m_solver = nullptr;
-        scoped_ptr<simple_solver>     m_owned_solver; // non-null when we own the solver
+        simple_solver&                m_solver;
 
     public:
-        // Construct without a custom solver; integer feasibility checks are skipped.
-        nielsen_graph(euf::sgraph& sg);
         // Construct with a caller-supplied solver.  Ownership is NOT transferred;
         // the caller is responsible for keeping the solver alive.
-        nielsen_graph(euf::sgraph& sg, simple_solver* solver);
+        nielsen_graph(euf::sgraph& sg, simple_solver& solver);
         ~nielsen_graph();
 
         euf::sgraph& sg() { return m_sg; }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index dee9aa4e9..4794fcbd7 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -34,7 +34,7 @@ namespace smt {
         m_egraph(ctx.get_manager()),
         m_sgraph(ctx.get_manager(), m_egraph),
         m_context_solver(ctx.get_manager()),
-        m_nielsen(m_sgraph, &m_context_solver),
+        m_nielsen(m_sgraph, m_context_solver),
         m_state(m_sgraph),
         m_regex(m_sgraph),
         m_model(*this, ctx.get_manager(), m_seq, m_rewriter, m_sgraph, m_regex)