diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 05d4d8efa..d0173f795 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -937,16 +937,15 @@ namespace seq {
     }
 
     void nielsen_graph::record_partial_derivative_edge(euf::snode* src_re, euf::snode* label, euf::snode* dst_re) {
-        if (!src_re || !dst_re || !src_re->get_expr() || !dst_re->get_expr())
-            return;
+        SASSERT(src_re && dst_re);
         if (!src_re->is_ground() || !dst_re->is_ground())
             return;
         if (src_re->is_fail() || dst_re->is_fail())
             return;
 
         euf::snode* label_re = to_partial_label_regex(label);
-        if (!label_re || !label_re->get_expr())
-            return;
+        SASSERT(label_re);
+
         if (!m_seq.is_re(label_re->get_expr()) || !label_re->is_ground())
             return;
 
@@ -3269,7 +3268,8 @@ namespace seq {
     // -----------------------------------------------------------------------
 
     void nielsen_graph::precompute_partial_dfa(euf::snode* root_re, const unsigned depth) {
-        if (!root_re || !root_re->is_ground())
+        SASSERT(root_re);
+        if (!root_re->is_ground())
             return;
 
         struct work_item { euf::snode* re; unsigned d; };
@@ -3284,6 +3284,7 @@ namespace seq {
             euf::snode_vector mts;
             m_sg.compute_minterms(re, mts);
             for (euf::snode* mt : mts) {
+                std::cout << "minterm: " << mk_pp(mt->get_expr(), m) << std::endl;
                 euf::snode* deriv = m_sg.brzozowski_deriv(re, mt);
                 if (!deriv || deriv->is_fail())
                     continue;
@@ -3294,6 +3295,8 @@ namespace seq {
                 }
             }
         }
+        std::string s = partial_dfa_to_dot(root_re, false);
+        std::cout << s << std::endl;
     }
 
     // -----------------------------------------------------------------------
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index e7555a42a..417296f44 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -493,36 +493,6 @@ namespace smt {
             return;
         }
 
-        if (!get_fparams().m_nseq_regex_factorization_threshold)
-            return;
-
-        //if (mem.m_regex->is_intersect()) {
-        //    // u \in r1 & r_2 → u \in r1 && u \in r2
-        //    for (const euf::snode* const arg : *mem.m_regex) {
-        //        expr_ref in_r(m_seq.re.mk_in_re(s, arg->get_expr()), m);
-        //        literal_vector lits;
-        //        lits.push_back(~mem.lit);
-        //        lits.push_back(mk_literal(in_r));
-        //        ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
-        //    }
-        //    m_ignored_mem.insert(mem.lit);
-        //    ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
-        //    return;
-        //}
-        //if (mem.m_regex->is_union()) {
-        //    // u \in r1 | r_2 → u \in r1 || u \in r2
-        //    literal_vector lits;
-        //    lits.push_back(~mem.lit);
-        //    for (const euf::snode* const arg : *mem.m_regex) {
-        //        expr_ref in_r(m_seq.re.mk_in_re(s, arg->get_expr()), m);
-        //        lits.push_back(mk_literal(in_r));
-        //    }
-        //    ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
-        //    m_ignored_mem.insert(mem.lit);
-        //    ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
-        //    return;
-        //}
-
         if (mem.m_regex->is_to_re()) {
             // u \in v (with v is constant) → u = v
             zstring str;
@@ -537,6 +507,9 @@ namespace smt {
             }
         }
 
+        if (!get_fparams().m_nseq_regex_factorization_threshold)
+            return;
+
         // Eager sigma factorization (token-level): when enabled, split a non-primitive
         // membership s ∈ r at the boundary between the first concat argument (head) and
         // the rest (tail), using compute_sigma. This mirrors the lazy Nielsen