diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py
index acd022a876..9861734b6c 100644
--- a/scripts/compare_seq_solvers.py
+++ b/scripts/compare_seq_solvers.py
@@ -37,7 +37,7 @@ COMMON_ARGS = ["model_validate=true"]
 # All three configurations are always run.
 SOLVERS = {
     "nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
-                "smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true", "smt.nseq.regex_dynamic_decomposition=false"],
+                "smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=false"],
     "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
                 "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=true"],
     "seq":     ["smt.string_solver=seq"],
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 2b835455ad..e8c30b9ce4 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -58,12 +58,13 @@ namespace seq {
         }
     }
 
-    // Normalize an arithmetic expression using th_rewriter.
+    // Normalize an arithmetic expression using the caller's th_rewriter.
     // Simplifies e.g. (n - 1 + 1) to n, preventing unbounded growth
-    // of power exponents during unwind/merge cycles.
-    static expr_ref normalize_arith(ast_manager &m, expr *e) {
-        expr_ref result(e, m);
-        th_rewriter rw(m);
+    // of power exponents during unwind/merge cycles.  Takes the rewriter as
+    // an argument (nielsen_graph::m_rw) — constructing a th_rewriter per
+    // call is far too expensive for these hot paths.
+    static expr_ref normalize_arith(th_rewriter &rw, expr *e) {
+        expr_ref result(e, rw.m());
         rw(result);
         return result;
     }
@@ -126,7 +127,7 @@ namespace seq {
         SASSERT(head && tail);
     }
 
-    std::pair<euf::snode const*, euf::snode const*> split_membership(euf::snode const *str, euf::snode const *regex, euf::sgraph& sg, unsigned threshold, split_set& result) {
+    std::pair<euf::snode const*, euf::snode const*> split_membership(euf::snode const *str, euf::snode const *regex, euf::sgraph& sg, seq_rewriter& rw, unsigned threshold, split_set& result) {
         ast_manager& m = sg.get_manager();
         euf::snode const* head;
         euf::snode const* tail;
@@ -140,7 +141,6 @@ namespace seq {
         // Decompose the regex into a split-set via the shared seq_split engine
         // (sigma from the paper): head ∈ Δ ∧ tail ∈ ∇ for each ⟨Δ,∇⟩, with the
         // lookahead oracle pruning non-viable ∇ during generation.
-        seq_rewriter rw(m);
         // "strong" might cause explosive behavior; better do this only in the saturation
         if (!rw.split(regex->get_expr(), result, threshold, split_mode::weak, oracle)) {
             result.clear();
@@ -283,12 +283,15 @@ namespace seq {
 
     // Right-derivative helper used by backward str_mem simplification:
     // dR(re, c) = reverse( derivative(c, reverse(re)) ).
-    static euf::snode const* reverse_brzozowski_deriv(euf::sgraph &sg, euf::snode const* re, euf::snode const* elem) {
+    // Takes the caller's persistent rewriters (nielsen_graph::m_deriv_rw /
+    // m_rw): this runs once per consumed suffix character, and constructing
+    // a seq_rewriter + th_rewriter per call dominated the simplification cost.
+    static euf::snode const* reverse_brzozowski_deriv(euf::sgraph &sg, seq_rewriter &rw, th_rewriter &tr,
+                                                      euf::snode const* re, euf::snode const* elem) {
         if (!re || !elem || !re->get_expr() || !elem->get_expr())
             return nullptr;
         ast_manager &m = sg.get_manager();
         seq_util &seq = sg.get_seq_util();
-        seq_rewriter rw(m);
 
         expr *elem_expr = elem->get_expr();
         expr *ch = nullptr;
@@ -300,7 +303,6 @@ namespace seq {
         if (!d.get())
             return nullptr;
         expr_ref result(seq.re.mk_reverse(d), m);
-        th_rewriter tr(m);
         tr(result);
         return sg.mk(result);
     }
@@ -380,6 +382,13 @@ namespace seq {
             // state — the view denotes ∅ regardless of the remaining string.
             if (m_regex->is_full_seq() && m_regex != m_root)
                 return true;
+            // An unresolved symbolic residual (ite / non-ground state, produced
+            // by consume_view stepping over a symbolic unit) is not a settled
+            // state: apply_regex_if_split may still resolve it to m_root, so no
+            // ε-verdict is possible yet.  (The plain branch below is guarded
+            // the same way implicitly: re_nullable is l_undef on such states.)
+            if (!m_regex->is_ground() || m_regex->kind() == euf::snode_kind::s_ite)
+                return false;
             // ε ∉ view when current state ≢ acceptance s
             return m_str->is_empty() && m_regex != m_root;
         }
@@ -574,6 +583,16 @@ namespace seq {
             }
             return;
         }
+        // Exprs are hash-consed, so pointer equality identifies duplicates.
+        // The bound queries in simplify_and_init (upper_bound/lower_bound via
+        // add_le_dependency) re-derive the same formula on every fixpoint
+        // sweep and on every re-simplification epoch; without this check the
+        // duplicates accumulate and each copy is re-asserted to the subsolver.
+        // Keeping the FIRST dep is sound: any recorded dep set entails its
+        // constraint, independently of the current outer assignment.
+        if (std::ranges::any_of(m_constraints,
+            [&](constraint const& e) { return e.fml.get() == c.fml.get(); }))
+            return;
         m_simplify_stamp = 0;
         m_constraints.push_back(c);
     }
@@ -757,7 +776,8 @@ namespace seq {
     nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver) :
         m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m),
         m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)),
-        m_seq_regex(alloc(seq::seq_regex, sg)), m_split_rw(sg.get_manager()), m_partial_dfa_pin(sg.get_manager()) {
+        m_seq_regex(alloc(seq::seq_regex, sg)), m_split_rw(sg.get_manager()), m_deriv_rw(sg.get_manager()),
+        m_partial_dfa_pin(sg.get_manager()) {
     }
 
     nielsen_graph::~nielsen_graph() {
@@ -861,6 +881,7 @@ namespace seq {
         m_depth_bound = 0;
         m_fresh_cnt = 0;
         m_root_constraints_asserted = false;
+        m_root_ic_asserted = 0;    // paired with the m_length_solver.reset() below
         // m_mod_cnt.reset();
         m_partial_dfa_edges.reset();
         m_partial_dfa_out.clear();
@@ -959,7 +980,7 @@ namespace seq {
     //          power(c^e) · char(c) → power(c^(e+1)),
     //          power(c^e1) · power(c^e2) → power(c^(e1+e2)).
     // Returns new snode if merging happened, nullptr otherwise.
-    static euf::snode const* merge_adjacent_powers(euf::sgraph& sg, euf::snode const* side) {
+    static euf::snode const* merge_adjacent_powers(euf::sgraph& sg, th_rewriter& rw, euf::snode const* side) {
         if (!side || side->is_empty() || side->is_token())
             return nullptr;
 
@@ -1026,7 +1047,7 @@ namespace seq {
                 }
                 if (local_merged) {
                     merged = true;
-                    expr_ref norm_exp = normalize_arith(m, exp_acc);
+                    expr_ref norm_exp = normalize_arith(rw, exp_acc);
                     expr_ref new_pow(seq.str.mk_power(base_e, norm_exp), m);
                     result.push_back(sg.mk(new_pow));
                 }
@@ -1064,7 +1085,7 @@ namespace seq {
                         break;
                     }
                     merged = true;
-                    expr_ref norm_exp = normalize_arith(m, exp_acc);
+                    expr_ref norm_exp = normalize_arith(rw, exp_acc);
                     expr_ref new_pow(seq.str.mk_power(base_e, norm_exp), m);
                     result.push_back(sg.mk(new_pow));
                     i = j;
@@ -1549,8 +1570,7 @@ namespace seq {
             // predicate is not internalized automatically (see the analogous
             // gradient propagation in theory_nseq).
             expr_ref div(a.mk_divides(a.mk_int(stride), a.mk_sub(len, a.mk_int(min_len))), m);
-            th_rewriter rw(m);
-            rw(div);
+            m_rw(div);
             e->add_side_constraint(mk_constraint(div, dep));
         }
     }
@@ -1765,9 +1785,9 @@ namespace seq {
                     continue;
 
                 // 3b: merge adjacent same-base tokens into combined powers
-                if (euf::snode const* s = merge_adjacent_powers(sg, eq.m_lhs))
+                if (euf::snode const* s = merge_adjacent_powers(sg, m_graph.m_rw, eq.m_lhs))
                     { eq.m_lhs = s; changed = true; }
-                if (euf::snode const* s = merge_adjacent_powers(sg, eq.m_rhs))
+                if (euf::snode const* s = merge_adjacent_powers(sg, m_graph.m_rw, eq.m_rhs))
                     { eq.m_rhs = s; changed = true; }
 
                 // 3c: CommPower-based power elimination — when one side starts
@@ -1803,7 +1823,7 @@ namespace seq {
                         if (!count.get() || consumed == 0)
                             continue;
 
-                        expr_ref norm_count = normalize_arith(m, count);
+                        expr_ref norm_count = normalize_arith(m_graph.m_rw, count);
                         bool pow_le_count = false, count_le_pow = false;
                         dep_tracker pow_le_dep = nullptr, count_le_dep = nullptr;
                         rational diff;
@@ -1829,13 +1849,13 @@ namespace seq {
                         }
                         else if (pow_le_count) {
                             // pow <= count: remainder goes to other_side
-                            expr_ref rem = normalize_arith(m, m_graph.a.mk_sub(norm_count, pow_exp));
+                            expr_ref rem = normalize_arith(m_graph.m_rw, m_graph.a.mk_sub(norm_count, pow_exp));
                             expr_ref pw(seq.str.mk_power(base_e, rem), m);
                             other_side = dir_concat(sg, sg.mk(pw), other_side, fwd);
                         }
                         else {
                             // count <= pow: remainder goes to pow_side
-                            expr_ref rem = normalize_arith(m, m_graph.a.mk_sub(pow_exp, norm_count));
+                            expr_ref rem = normalize_arith(m_graph.m_rw, m_graph.a.mk_sub(pow_exp, norm_count));
                             expr_ref pw(seq.str.mk_power(base_e, rem), m);
                             pow_side = dir_concat(sg, sg.mk(pw), pow_side, fwd);
                         }
@@ -1942,7 +1962,7 @@ namespace seq {
                     euf::snode const* src_re = mem.m_regex;
                     euf::snode const* deriv = fwd
                         ? sg.brzozowski_deriv(mem.m_regex, tok)
-                        : reverse_brzozowski_deriv(sg, mem.m_regex, tok);
+                        : reverse_brzozowski_deriv(sg, m_graph.m_deriv_rw, m_graph.m_rw, mem.m_regex, tok);
                     TRACE(seq, tout << mem_pp(mem) << " d: " << spp(deriv, m) << "\n");
                     if (!deriv)
                         break;
@@ -2108,8 +2128,7 @@ namespace seq {
 
     euf::snode const* nielsen_graph::mk_rewrite(expr* e) const {
         expr_ref er(e, m);
-        th_rewriter rw(m);
-        rw(er);
+        m_rw(er);
         return m_sg.mk(er);
     }
 
@@ -2823,6 +2842,28 @@ namespace seq {
         return any_of(tokens, [var](auto const &t) { return t == var; });
     }
 
+#ifdef Z3DEBUG
+    // Deep occurrence check: does `var` occur anywhere in `n`, INCLUDING
+    // inside power bases?  collect_tokens treats a power token as opaque, so
+    // neither nielsen_subst's ctor assertion nor is_eliminating() can see an
+    // occurrence nested inside a base — such a substitution would silently be
+    // non-eliminating and its |x| = |replacement| edge constraint wrong.  All
+    // power bases are ground w.r.t. the substituted variable by construction
+    // today (gpower prefixes stop at the first variable); the assertions at
+    // the power-substitution sites pin that invariant down.
+    static bool deep_contains_var(euf::snode const* n, euf::snode const* var) {
+        euf::snode_vector tokens;
+        n->collect_tokens(tokens);
+        for (euf::snode const* t : tokens) {
+            if (t == var)
+                return true;
+            if (t->is_power() && t->arg0() && deep_contains_var(t->arg0(), var))
+                return true;
+        }
+        return false;
+    }
+#endif
+
     bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
         // resist the temptation to add rules that "simplify" primitive membership constraints!
         // pretty much all of them could cause divergence!
@@ -3481,8 +3522,6 @@ namespace seq {
             euf::snode const* eq1_rhs = rhs_prefix;
             euf::snode const* eq2_lhs = lhs_suffix;
             euf::snode const* eq2_rhs = rhs_suffix;
-            th_rewriter rw(m);
-
 
             euf::snode const* pad = nullptr;
             if (padding != 0) {
@@ -3959,7 +3998,7 @@ namespace seq {
                     if (!count.get() || consumed == 0)
                         continue;
 
-                    expr_ref norm_count = normalize_arith(m, count);
+                    expr_ref norm_count = normalize_arith(m_rw, count);
 
                     // Skip if ordering is already deterministic — simplify_and_init
                     // pass 3c should have handled it.
@@ -4035,7 +4074,7 @@ namespace seq {
         expr *power_e = power->get_expr();
         SASSERT(power_e);
         expr *base_expr = to_app(power_e)->get_arg(0);
-        const expr_ref n_minus_1 = normalize_arith(m, a.mk_sub(exp_n, one));
+        const expr_ref n_minus_1 = normalize_arith(m_rw, a.mk_sub(exp_n, one));
         const expr_ref nested_pow(seq.str.mk_power(base_expr, n_minus_1), m);
         euf::snode const* nested_power_snode = m_sg.mk(nested_pow);
 
@@ -4343,7 +4382,7 @@ namespace seq {
                 }
                 // x2 = x[|x1|+1:]  (slice tail after the landed prefix and the char)
                 const expr_ref after =
-                    normalize_arith(m, a.mk_add(compute_length_expr(x1).get(), a.mk_int(1)));
+                    normalize_arith(m_rw, a.mk_add(compute_length_expr(x1).get(), a.mk_int(1)));
                 euf::snode const* x2 = get_tail(x, after.get());
                 euf::snode const* repl = m_sg.mk_concat(x1, m_sg.mk_concat(aunit, x2));
 
@@ -4881,7 +4920,10 @@ namespace seq {
 
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, "power intr", true);
-            nielsen_subst s(var, replacement, eq.m_dep); // TODO review - ensure var does not occur in replacement.
+            // The replacement is built from power tokens whose bases must not
+            // contain `var` (deep check: collect_tokens is opaque to bases).
+            SASSERT(!deep_contains_var(replacement, var));
+            nielsen_subst s(var, replacement, eq.m_dep);
             e->add_subst(s);
             child->apply_subst(m_sg, s);
 
@@ -5058,12 +5100,13 @@ namespace seq {
     }
 
     bool nielsen_graph::apply_regex_if_split(nielsen_node *node) {
+        bool_rewriter brw(m);
         for (str_mem const &mem : node->str_mems()) {
             SASSERT(mem.well_formed());
 
             expr *r_expr = mem.m_regex->get_expr();
             expr_ref c(m), th(m), el(m);
-            if (!bool_rewriter(m).decompose_ite(r_expr, c, th, el))
+            if (!brw.decompose_ite(r_expr, c, th, el))
                 continue;
 
             bool created = false;
@@ -5082,7 +5125,7 @@ namespace seq {
                     continue;
 
                 expr_ref c2(m), th2(m), el2(m);
-                if (!bool_rewriter(m).decompose_ite(r, c2, th2, el2)) {
+                if (!brw.decompose_ite(r, c2, th2, el2)) {
                     // No ite remaining: leaf → create child node with regex updated to r.
                     // Canonicalize with th_rewriter so that the resolved leaf shares
                     // its snode id with the corresponding partial-DFA state (which is
@@ -5104,9 +5147,8 @@ namespace seq {
                     continue;
                 }
 
-                th_rewriter tr(m);
                 expr_ref c_simp(c2, m);
-                tr(c_simp);
+                m_rw(c_simp);
 
                 if (m.is_true(c_simp)) {
                     if (!m_seq.re.is_empty(th2))
@@ -5132,6 +5174,17 @@ namespace seq {
 
             if (created)
                 return true;
+
+            // The worklist only ever prunes ∅ branches, so no created child
+            // means every valuation of the ite conditions collapses the regex
+            // to ∅ — the membership is unsatisfiable outright.  Report the
+            // definite regex conflict instead of falling through to weaker
+            // modifiers (or, for a view state, to none at all → VERIFY(ext)).
+            // Justified by the membership alone: the conditions are part of
+            // the regex itself.
+            node->set_general_conflict();
+            node->set_conflict(backtrack_reason::regex, mem.m_dep);
+            return true;
         }
         return false;
     }
@@ -5313,7 +5366,10 @@ namespace seq {
 
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, "power split", true);
-                nielsen_subst s(var_head, replacement, eq->m_dep); // TODO review - ensure var does not occur in replacement.
+                // deep check: the power bases in the replacement must not
+                // contain var_head (collect_tokens is opaque to bases)
+                SASSERT(!deep_contains_var(replacement, var_head));
+                nielsen_subst s(var_head, replacement, eq->m_dep);
                 e->add_subst(s);
                 child->apply_subst(m_sg, s);
 
@@ -5343,6 +5399,7 @@ namespace seq {
             euf::snode const* replacement = dir_concat(m_sg, power, tail, fwd);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, "power split", false);
+            SASSERT(!deep_contains_var(replacement, var_head));
             const nielsen_subst s(var_head, replacement, eq->m_dep);
             e->add_subst(s);
             // |x'| >= 0, i.e. |x| >= n·|u| (the branch condition)
@@ -5397,7 +5454,8 @@ namespace seq {
             euf::snode const* replacement = dir_concat(m_sg, base, power_snode, fwd);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, "unwinding eq &gt;", false);
-            const nielsen_subst s(power, replacement, eq->m_dep); // TODO review - ensure var does not occur in replacement.
+            SASSERT(!deep_contains_var(replacement, power));
+            const nielsen_subst s(power, replacement, eq->m_dep);
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), eq->m_dep));
@@ -5441,7 +5499,8 @@ namespace seq {
             euf::snode const* replacement = dir_concat(m_sg, base, power_snode, fwd);
             nielsen_node* child = mk_child(node);
             nielsen_edge* e = mk_edge(node, child, "unwinding mem &gt;", false);
-            const nielsen_subst s(power, replacement, mem->m_dep); // TODO review - ensure var does not occur in replacement.
+            SASSERT(!deep_contains_var(replacement, power));
+            const nielsen_subst s(power, replacement, mem->m_dep);
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             e->add_side_constraint(mk_constraint(a.mk_ge(exp_n, one), mem->m_dep));
@@ -5716,7 +5775,6 @@ namespace seq {
         SASSERT(var && var->is_var());
         //unsigned mc = 0;
         //m_mod_cnt.find(var->id(), mc);
-        th_rewriter rw(m);
         return m_sk.mk("gpn!", var->get_expr()/*, a.mk_int(mc)*/, a.mk_int());
     }
 
@@ -5724,7 +5782,6 @@ namespace seq {
         SASSERT(var && var->is_var());
         //unsigned mc = 0;
         //m_mod_cnt.find(var->id(), mc);
-        th_rewriter rw(m);
         return m_sk.mk("gpm!", var->get_expr()/*, a.mk_int(mc)*/, a.mk_int());
     }
 
@@ -5761,17 +5818,29 @@ namespace seq {
         // an assumption/dep slot per constraint, on every visit.
         if (from_idx == UINT_MAX)
             from_idx = node->m_parent_ic_count;
-        for (unsigned i = from_idx; i < node->constraints().size(); ++i) {
+        // The ROOT's constraints are asserted at the sub-solver's BASE level,
+        // which is never popped between deepening iterations or across hot
+        // restarts (until the solver itself is reset).  Skip the prefix that is
+        // already in the solver: each redundant re-assertion would permanently
+        // burn one assumption literal + kernel clause per constraint
+        // (sub_solver::assert_expr) and grow every subsequent check().
+        const bool is_root = node == m_root;
+        if (is_root)
+            from_idx = std::max(from_idx, m_root_ic_asserted);
+        unsigned i = from_idx;
+        for (; i < node->constraints().size(); ++i) {
             auto& c = node->constraints()[i];
             auto lit = m_context_solver.literal_if_false(c.fml);
             // std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" <<
             // std::endl;
             if (lit != sat::null_literal) {
                 node->set_external_conflict(lit, c.dep);
-                return;
+                break;   // constraints [from_idx, i) were asserted, i was not
             }
             assert_to_subsolver(c);
         }
+        if (is_root && i > m_root_ic_asserted)
+            m_root_ic_asserted = i;
     }
 
     void nielsen_graph::generate_node_length_constraints(nielsen_node* node) {
@@ -6151,6 +6220,18 @@ namespace seq {
     //          an undecided component could wrongly report emptiness).
     // -----------------------------------------------------------------------
 
+    // FNV-style hash for the visited-key encoding of a product state.  The
+    // engines below run with budgets of several thousand states per call; an
+    // ordered std::set would pay an O(len·log n) vector comparison per probe.
+    struct prod_key_hash {
+        size_t operator()(std::vector<unsigned> const& v) const {
+            size_t h = 0xcbf29ce484222325ull;
+            for (unsigned x : v)
+                h = (h ^ x) * 0x100000001b3ull;
+            return h;
+        }
+    };
+
     lbool nielsen_graph::check_concat_product_emptiness(vector<vector<prod_comp>> const& factors,
                                                         prod_comp const& rhs, unsigned max_states) {
         const unsigned k = factors.size();
@@ -6171,7 +6252,7 @@ namespace seq {
             return key;
         };
 
-        std::set<std::vector<unsigned>> visited;
+        std::unordered_set<std::vector<unsigned>, prod_key_hash> visited;
         vector<cstate> work;
 
         auto push_state = [&](unsigned idx, vector<prod_comp> const& comps, prod_comp const& r) {
@@ -6192,7 +6273,7 @@ namespace seq {
                 return l_undef;
             if (explored >= max_states)
                 return l_undef;
-            const cstate cur = work.back();
+            const cstate cur = std::move(work.back());
             work.pop_back();
             ++explored;
 
@@ -6313,7 +6394,7 @@ namespace seq {
             return key;
         };
 
-        std::set<std::vector<unsigned>> visited;
+        std::unordered_set<std::vector<unsigned>, prod_key_hash> visited;
         // BFS (vector + head index) for a SHORTEST accepting word.
         vector<std::pair<vector<prod_comp>, zstring>> work;
         work.push_back({ comps0, zstring() });
@@ -6324,8 +6405,9 @@ namespace seq {
         while (head < work.size()) {
             if (!m.inc() || head >= MAX_STATES)
                 return false;
-            vector<prod_comp> cur = work[head].first;
-            zstring w = work[head].second;
+            // move out: the BFS never revisits an entry behind `head`
+            vector<prod_comp> cur = std::move(work[head].first);
+            zstring w = std::move(work[head].second);
             ++head;
 
             bool any_dead = false;
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 26b486d0e1..ef2c71650e 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -161,7 +161,9 @@ namespace seq {
     // decompose a membership constraint into a set of pairs of regex splits.
     // Eagerly materialises the full split-set (used by the eager propagation path
     // in theory_nseq::propagate_pos_mem); the lazy Nielsen path uses rf_state.
-    std::pair<euf::snode const*, euf::snode const*> split_membership(euf::snode const* str, euf::snode const* regex, euf::sgraph& sg, unsigned threshold, split_set& result);
+    // `rw` is the caller's persistent split engine (constructing a seq_rewriter
+    // per call is expensive).
+    std::pair<euf::snode const*, euf::snode const*> split_membership(euf::snode const* str, euf::snode const* regex, euf::sgraph& sg, seq_rewriter& rw, unsigned threshold, split_set& result);
 
     // Lookahead oracle for the split engine: is the split's right component
     // `n_regex` prefix-compatible with the constant character sequence `c`?
@@ -909,7 +911,12 @@ namespace seq {
         arith_util                    a;
         seq_util&                     m_seq;
         euf::sgraph&                  m_sg;
-        th_rewriter                   m_rw;
+        // Shared rewriter for all hot paths (arith normalization, leaf
+        // canonicalization, divisibility rewriting).  Constructing a fresh
+        // th_rewriter allocates the full rewriter core — never do that per
+        // call inside search/simplify loops; use this member (mutable so
+        // const helpers like mk_rewrite can canonicalize).
+        mutable th_rewriter           m_rw;
         arith_rewriter                m_a_rw;
         skolem                        m_sk;
         ptr_vector<nielsen_node>      m_nodes;
@@ -951,6 +958,17 @@ namespace seq {
         // Set to true after assert_root_constraints_to_solver() is first called.
         bool                          m_root_constraints_asserted = false;
 
+        // Number of root-node constraints already asserted into the sub-solver.
+        // Root assertions live at the solver's BASE level, which is never popped
+        // between deepening iterations (nor across hot restarts until the solver
+        // itself is reset), so re-asserting the prefix on every search_dfs(root)
+        // entry would permanently burn one assumption literal + kernel clause
+        // per constraint per iteration (sub_solver::assert_expr), growing every
+        // subsequent check().  Maintained by assert_node_side_constraints; reset
+        // together with the sub-solver (reset / reset_length_solver).  mutable:
+        // assert_node_side_constraints is const.
+        mutable unsigned              m_root_ic_asserted = 0;
+
         // Parikh image filter: generates modular length constraints from regex
         // memberships.  Allocated in the constructor; owned by this graph.
         seq_parikh*                   m_parikh = nullptr;
@@ -964,6 +982,13 @@ namespace seq {
         // suspended split iterators stored in m_rf_states stay valid across
         // search_dfs recursion and iterative deepening.
         seq_rewriter            m_split_rw;
+        // Dedicated seq_rewriter for reverse Brzozowski derivatives (backward
+        // character consumption in simplify_and_init).  Kept separate from
+        // m_split_rw so derivative calls are never interleaved with the
+        // suspended split iterators that reference that engine, and reused
+        // across calls (a fresh seq_rewriter per consumed character was a
+        // dominant simplification cost).
+        seq_rewriter            m_deriv_rw;
         // Owns the suspended factorization continuations (rf_state); nodes hold
         // raw pointers into this pool.  Freed in reset().
         ptr_vector<rf_state>    m_rf_states;
@@ -1159,6 +1184,17 @@ namespace seq {
         // skolem that cannot be represented (e.g. a power token); the node is then skipped.
         expr_ref clean_harvest_expr(expr* e, bool& ok);
 
+        // Reset the arithmetic sub-solver together with the graph-side
+        // bookkeeping that tracks what has been asserted into it (the root
+        // constraints asserted at its base level).  Callers must use this
+        // instead of resetting the sub-solver directly — otherwise the next
+        // search would skip re-asserting the root constraints into the fresh
+        // solver (see m_root_ic_asserted).
+        void reset_length_solver() {
+            m_length_solver.reset();
+            m_root_ic_asserted = 0;
+        }
+
         // display for debugging
         std::ostream& display(std::ostream& out) const;
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index f4ee1be8aa..8444779fe4 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -40,7 +40,9 @@ namespace smt {
         m_axioms(m_th_rewriter),
         m_regex(m_sg),
         m_model(m, ctx, m_seq, m_rewriter, m_sg),
-        m_relevant_lengths(m)
+        m_relevant_lengths(m),
+        m_gradient_pin(m),
+        m_nonneg_cache(m)
     {
         std::function<void(expr_ref_vector const&)> add_clause =
             [&](expr_ref_vector const &clause) {
@@ -84,8 +86,14 @@ namespace smt {
         m_axioms.set_ensure_digits(ensure_digit_axiom);
         m_axioms.set_mark_no_diseq(mark_no_diseq);
 
-        m_context_solver.m_should_internalize = true; // delete this if using internalize as fallback
-       
+        // m_should_internalize stays false by default: with it permanently on,
+        // literal_if_false internalized EVERY side constraint of EVERY explored
+        // DFS node into the main context (bool vars/enodes/arith atoms for
+        // branches that are immediately backtracked, never reclaimed within the
+        // search).  Internalization is instead escalated lazily by
+        // add_nielsen_assumptions when a SAT-leaf assumption turns out false —
+        // the retry loop there re-solves with internalization enabled, and
+        // literal_if_false then rejects the stale leaf via an external conflict.
     }
 
     // -----------------------------------------------------------------------
@@ -706,7 +714,7 @@ namespace smt {
             const unsigned threshold = get_fparams().m_nseq_regex_factorization_threshold;
 
             split_set pairs;
-            auto [head, tail] = seq::split_membership(mem.m_str, mem.m_regex, m_sg, threshold, pairs);
+            auto [head, tail] = seq::split_membership(mem.m_str, mem.m_regex, m_sg, m_rewriter, threshold, pairs);
 
             if (!head) {
                 // gave up
@@ -846,7 +854,7 @@ namespace smt {
                 m_nielsen.add_str_eq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r);
                 ++num_eqs;
             }
-            if (std::holds_alternative<deq_item>(item)) {
+            else if (std::holds_alternative<deq_item>(item)) {
                 SASSERT(!get_fparams().m_nseq_axiomatize_diseq);
                 auto const& deq = std::get<deq_item>(item);
                 m_nielsen.add_str_deq(deq.m_lhs, deq.m_rhs, deq.lit);
@@ -992,7 +1000,10 @@ namespace smt {
                     }
                 }
                 m_nielsen.clear_sat_node();
-                m_length_solver.reset();
+                // resets the sub-solver AND the graph's root-assertion watermark
+                // (the next search must re-assert the root constraints into the
+                // fresh solver)
+                m_nielsen.reset_length_solver();
             }
             else {
                 // let's rebuild the whole Nielsen graph
@@ -1367,20 +1378,44 @@ namespace smt {
 #endif
     }
 
-    void theory_nseq::set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const {
+    void theory_nseq::set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) {
         TRACE(seq, tout << "nseq conflict: " << eqs.size() << " eqs, " << lits.size() << " lits\n";
               for (auto lit : lits) tout << ctx.literal2expr(lit) << "\n";
               for (auto [a, b] : eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";
         );
 
-        SASSERT(std::ranges::all_of(eqs, [&](auto& eq) { return eq.first->get_root() == eq.second->get_root(); }));
+        // The premises are normally all on the trail (lits true, eqs merged).
+        // After a hot restart, however, a retained (general) conflict node may
+        // cite an OUTER arithmetic bound literal that has been retracted since
+        // it was recorded: the pop tracking (m_last_constraint_added) only
+        // covers string constraints, while bound literals enter conflict deps
+        // through the context-solver queries in simplification (upper/lower
+        // bound, check_lp_le).  The derived lemma is still valid — the cited
+        // premises entail false regardless of the current assignment — but an
+        // eager conflict justification requires every premise on the trail, so
+        // fall back to asserting the clause as a theory axiom in that case
+        // (mirrors set_propagate).
+        const bool all_on_trail =
+            all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }) &&
+            std::ranges::all_of(eqs, [&](auto& eq) { return eq.first->get_root() == eq.second->get_root(); });
 
-        SASSERT(all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }));
+        if (all_on_trail) {
+            ctx.set_conflict(
+                ctx.mk_justification(
+                    ext_theory_conflict_justification(
+                        get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
+            return;
+        }
 
-        ctx.set_conflict(
-            ctx.mk_justification(
-                ext_theory_conflict_justification(
-                    get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), 0, nullptr)));
+        TRACE(seq, tout << "nseq conflict cites retracted premises; asserting as theory axiom\n");
+        literal_vector clause;
+        for (literal lit : lits)
+            clause.push_back(~lit);
+        for (auto [a, b] : eqs)
+            clause.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
+        for (auto lit : clause)
+            ctx.mark_as_relevant(lit);
+        ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
     }
 
     void theory_nseq::set_propagate(enode_pair_vector const& eqs, literal_vector const& lits, literal p) {
@@ -1702,15 +1737,26 @@ namespace smt {
     }
 
     bool theory_nseq::assert_nonneg_for_all_vars() {
-        arith_util arith(m);
         bool new_axiom = false;
         unsigned nv = get_num_vars();
+        // This runs on every final_check over ALL theory vars; cache the
+        // (>= (str.len e) 0) formula per var index.  Theory-var indices are
+        // recycled across pops, so validate the cached entry against the
+        // enode's expr: the pinned formula keeps its subterm alive, hence an
+        // equal pointer is necessarily the same (hash-consed) expr.
+        if (m_nonneg_key.size() < nv) {
+            m_nonneg_key.resize(nv, nullptr);
+            m_nonneg_cache.resize(nv);
+        }
         for (unsigned v = 0; v < nv; ++v) {
             expr* e = get_enode(v)->get_expr();
             if (!m_seq.is_seq(e))
                 continue;
-            expr_ref len_var(m_seq.str.mk_length(e), m);
-            expr_ref ge_zero(arith.mk_ge(len_var, arith.mk_int(0)), m);
+            if (m_nonneg_key[v] != e) {
+                m_nonneg_key[v] = e;
+                m_nonneg_cache.set(v, m_autil.mk_ge(m_seq.str.mk_length(e), m_autil.mk_int(0)));
+            }
+            expr* ge_zero = m_nonneg_cache.get(v);
             if (!ctx.b_internalized(ge_zero))
                 ctx.internalize(ge_zero, true);
             literal lit = ctx.get_literal(ge_zero);
@@ -2078,8 +2124,12 @@ namespace smt {
             unsigned g = 1;
             if (m_gradient_cache.contains(s))
                 g = m_gradient_cache[s];
-            else
+            else {
                 m_gradient_cache.insert(s, 1);
+                // the cache is not trailed; pin the key so it cannot dangle
+                // after a pop releases the term (see m_gradient_pin)
+                m_gradient_pin.push_back(s);
+            }
 
             expr_ref allchar(m_seq.re.mk_full_char(m_seq.re.mk_re(m_sg.get_str_sort())), m);
             expr_ref l_expr(m_autil.mk_int(l), m);
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index 85aec28224..f3c6d9f1f2 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -65,6 +65,18 @@ namespace smt {
         hashtable<literal, obj_hash<literal>, default_eq<literal>>    m_ignored_mem;     // track membership constraints that should not be passed to Nielsen
         expr_ref_vector         m_relevant_lengths;     // track variables whose lengths are relevant
         obj_map<expr, unsigned> m_gradient_cache;
+        // Pins the keys of m_gradient_cache: the cache is deliberately not
+        // trailed (the gradient escalation must survive backtracking), so its
+        // expr* keys would otherwise dangle once a pop releases the length
+        // argument.  Grows monotonically, bounded by the number of distinct
+        // length-relevant terms.
+        expr_ref_vector         m_gradient_pin;
+        // assert_nonneg_for_all_vars cache: per theory var v, the enode expr
+        // the entry was built for (m_nonneg_key, validated by pointer — safe
+        // because the pinned ge-expr keeps its subterm alive, so an equal
+        // pointer is the same expr) and the pinned (>= (str.len e) 0) formula.
+        ptr_vector<expr>        m_nonneg_key;
+        expr_ref_vector         m_nonneg_cache;
         sat::literal_vector     m_nielsen_literals;   // literals created by a Nilsen check
         sat::literal            m_assumption_lit;     // literal used as assumption to bound search to selected literal assignments
         unsigned                m_max_unfolding_depth = 0;
@@ -94,10 +106,6 @@ namespace smt {
         unsigned m_num_length_axioms    = 0;
         bool     m_digits_initialized   = false;
 
-        // map from context enode to private sgraph snode
-        obj_map<expr, euf::snode*> m_expr2snode;
-
-
         // higher-order terms (seq.map, seq.mapi, seq.foldl, seq.foldli)
         ptr_vector<app>  m_ho_terms;
         unsigned         m_num_ho_unfolds = 0;
@@ -151,7 +159,11 @@ namespace smt {
         // literals so the SAT solver tries a different one.  Returns false if there
         // is nothing to block (empty clause).  Intentionally unsound.
         bool block_current_assignment();
-        void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const;
+        // Not const: when a cited premise is no longer on the trail (a hot
+        // restart can retain conflicts citing since-retracted outer bound
+        // literals), the conflict falls back to a theory-axiom clause, which
+        // internalizes equalities via mk_eq.
+        void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
         void set_conflict(literal_vector const& lits) {
             const enode_pair_vector eqs;
             set_conflict(eqs, lits);