diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 38049c640..8498cdfb7 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -104,7 +104,6 @@ namespace seq {
     void str_eq::sort() {
         if (m_lhs && m_rhs && m_lhs->id() > m_rhs->id()) {
             std::swap(m_lhs, m_rhs);
-            std::swap(m_l, m_r);
         }
     }
 
@@ -199,15 +198,13 @@ namespace seq {
         m_char_ranges.reset();
         m_var_lb.reset();
         m_var_ub.reset();
-        for (auto const& eq : parent.m_str_eq) {
-            m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs,eq.m_l, eq.m_r, eq.m_dep));
-        }
-        for (auto const& mem : parent.m_str_mem) {
-            m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_lit, mem.m_history, mem.m_id, mem.m_dep));
-        }
-        for (auto const& ic : parent.m_int_constraints) {
+        for (auto const& eq : parent.m_str_eq)
+            m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs, eq.m_dep));
+        for (auto const& mem : parent.m_str_mem)
+            m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_history, mem.m_id, mem.m_dep));
+        for (auto const& ic : parent.m_int_constraints)
             m_int_constraints.push_back(ic);
-        }
+        
         // clone character disequalities
         for (auto const& kv : parent.m_char_diseqs) {
             ptr_vector<euf::snode> diseqs;
@@ -331,7 +328,7 @@ namespace seq {
             return true;
         }
         // add int_constraint: len(var) >= lb
-        ast_manager& m = m_graph.m();
+        ast_manager& m = m_graph.get_manager();
         seq_util& seq = m_graph.seq();
         arith_util arith(m);
         expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
@@ -357,7 +354,7 @@ namespace seq {
             return true;
         }
         // add int_constraint: len(var) <= ub
-        ast_manager& m = m_graph.m();
+        ast_manager& m = m_graph.get_manager();
         seq_util& seq = m_graph.seq();
         arith_util arith(m);
         expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
@@ -461,7 +458,7 @@ namespace seq {
             }
             else {
                 // str is a concatenation or other term: add as general int_constraints
-                ast_manager& m = m_graph.m();
+                ast_manager& m = m_graph.get_manager();
                 arith_util arith(m);
                 expr_ref len_str = m_graph.compute_length_expr(mem.m_str);
                 if (min_len > 0) {
@@ -537,7 +534,7 @@ namespace seq {
     // -----------------------------------------------
 
     nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver):
-        m_m(sg.get_manager()),
+        m(sg.get_manager()),
         m_seq(sg.get_seq_util()),
         m_sg(sg),
         m_solver(solver),
@@ -577,7 +574,7 @@ namespace seq {
         if (!m_root)
             m_root = mk_node();
         dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
-        str_eq eq(lhs, rhs, l, r, dep);
+        str_eq eq(lhs, rhs, dep);
         eq.sort();
         m_root->add_str_eq(eq);
     }
@@ -588,7 +585,7 @@ namespace seq {
         dep_tracker dep = m_dep_mgr.mk_leaf(l);
         euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
         unsigned id = next_mem_id();
-        m_root->add_str_mem(str_mem(str, regex, l, history, id, dep));
+        m_root->add_str_mem(str_mem(str, regex, history, id, dep));
     }
 
     void nielsen_graph::inc_run_idx() {
@@ -892,9 +889,9 @@ namespace seq {
     // Groups consecutive s_char tokens into quoted strings, renders s_var by name,
     // shows s_power with superscripts, s_unit by its inner expression,
     // and falls back to mk_pp (HTML-escaped) for other token kinds.
-    std::string snode_label_html(euf::snode const* n, ast_manager& m) {
-        if (!n)
-            return "null";
+
+    static std::string snode_label_html(euf::snode const* n, ast_manager& m) {
+        if (!n) return "null";
         seq_util seq(m);
 
         // collect all leaf tokens left-to-right
@@ -2287,7 +2284,7 @@ namespace seq {
             // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
             m_depth_bound = 3;
             while (true) {
-                if (!m().inc()) {
+                if (!m.inc()) {
 #ifdef Z3DEBUG
                     // Examining the Nielsen graph is probably the best way of debugging
                     std::string dot = to_dot();
@@ -2335,7 +2332,7 @@ namespace seq {
         m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
 
         // check for external cancellation (timeout, user interrupt)
-        if (!m().inc())
+        if (!m.inc())
             return search_result::unknown;
 
         // check DFS node budget (0 = unlimited)
@@ -2537,8 +2534,9 @@ namespace seq {
                 if (!lhead || !rhead)
                     continue;
 
-                // char vs var: branch 1: var -> ε, branch 2: var -> char·var
-                euf::snode* char_head = lhead->is_unit() ? lhead : (rhead->is_unit() ? rhead : nullptr);
+                // char vs var: branch 1: var -> ε, branch 2: var -> char·var   (depending on direction)
+                // NSB review: add also case var -> unit·var
+                euf::snode* char_head = lhead->is_char() ? lhead : (rhead->is_char() ? rhead : nullptr);
                 euf::snode* var_head = lhead->is_var() ? lhead : (rhead->is_var() ? rhead : nullptr);
                 if (char_head && var_head) {
                     nielsen_node* child = mk_child(node);
@@ -2861,8 +2859,8 @@ namespace seq {
             auto& eqs = child->str_eqs();
             eqs[eq_idx] = eqs.back();
             eqs.pop_back();
-            eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_l, eq.m_r, eq.m_dep));
-            eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_l, eq.m_r, eq.m_dep));
+            eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_dep));
+            eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_dep));
 
             // Int constraints on the edge.
             // 1) len(pad) = |padding|  (if padding variable was created)
@@ -3411,11 +3409,11 @@ namespace seq {
             nielsen_node* child = mk_child(node);
 
             // Add membership: pr ∈ stab_base* (stabilizer constraint)
-            child->add_str_mem(str_mem(pr, star_sn, mem.m_lit, mem.m_history, next_mem_id(), mem.m_dep));
+            child->add_str_mem(str_mem(pr, star_sn, mem.m_history, next_mem_id(), mem.m_dep));
 
             // Add remaining membership: po · tail ∈ R (same regex, trimmed history)
             euf::snode* post_tail = str_tail->is_empty() ? po : m_sg.mk_concat(po, str_tail);
-            child->add_str_mem(str_mem(post_tail, mem.m_regex, mem.m_lit, nullptr, next_mem_id(), mem.m_dep));
+            child->add_str_mem(str_mem(post_tail, mem.m_regex, nullptr, next_mem_id(), mem.m_dep));
 
             // Blocking constraint: po must NOT start with stab_base
             // po ∈ complement(non_nullable(stab_base) · Σ*)
@@ -3427,7 +3425,7 @@ namespace seq {
                 expr_ref block_re(seq.re.mk_complement(base_then_all), mgr);
                 euf::snode* block_sn = m_sg.mk(block_re);
                 if (block_sn)
-                    child->add_str_mem(str_mem(po, block_sn, mem.m_lit, nullptr, next_mem_id(), mem.m_dep));
+                    child->add_str_mem(str_mem(po, block_sn, nullptr, next_mem_id(), mem.m_dep));
             }
 
             // Substitute x → pr · po
@@ -3925,6 +3923,7 @@ namespace seq {
         }
     }
 
+    #if 0
     void nielsen_graph::explain_conflict(svector<std::pair<smt::enode*, smt::enode*>>& eqs, 
         svector<sat::literal>& mem_literals) const {
         SASSERT(m_root);
@@ -3939,6 +3938,7 @@ namespace seq {
                 mem_literals.push_back(std::get<sat::literal>(d));
         }
     }
+    #endif
 
     // -----------------------------------------------------------------------
     // nielsen_graph: length constraint generation
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 90f957d0a..8b82ffe6c 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -353,12 +353,12 @@ namespace seq {
     struct str_eq {
         euf::snode* m_lhs;
         euf::snode* m_rhs;
-        smt::enode *m_l, *m_r;
         dep_tracker m_dep;
 
-        str_eq(): m_lhs(nullptr), m_rhs(nullptr), m_dep(nullptr) {}
-        str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r, dep_tracker const& dep):
-            m_lhs(lhs), m_rhs(rhs), m_l(l), m_r(r), m_dep(dep) {}
+
+        str_eq() = default;
+        str_eq(euf::snode* lhs, euf::snode* rhs, dep_tracker const& dep):
+            m_lhs(lhs), m_rhs(rhs), m_dep(dep) {}
 
         bool operator==(str_eq const& other) const {
             return m_lhs == other.m_lhs && m_rhs == other.m_rhs;
@@ -379,14 +379,13 @@ namespace seq {
     struct str_mem {
         euf::snode* m_str;
         euf::snode* m_regex;
-        sat::literal m_lit;
         euf::snode* m_history;  // tracks derivation history for cycle detection
         unsigned    m_id;       // unique identifier
         dep_tracker m_dep;
 
         str_mem(): m_str(nullptr), m_regex(nullptr), m_history(nullptr), m_id(UINT_MAX), m_dep(nullptr) {}
-        str_mem(euf::snode* str, euf::snode* regex, sat::literal l, euf::snode* history, unsigned id, dep_tracker const& dep):
-            m_str(str), m_regex(regex), m_lit(l), m_history(history), m_id(id), m_dep(dep) {}
+        str_mem(euf::snode* str, euf::snode* regex, euf::snode* history, unsigned id, dep_tracker const& dep):
+            m_str(str), m_regex(regex), m_history(history), m_id(id), m_dep(dep) {}
 
         bool operator==(str_mem const& other) const {
             return m_id == other.m_id && m_str == other.m_str && m_regex == other.m_regex;
@@ -747,7 +746,7 @@ namespace seq {
     // mirrors ZIPT's NielsenGraph
     class nielsen_graph {
         friend class nielsen_node;
-        ast_manager&                  m_m;
+        ast_manager&                  m;
         seq_util&                     m_seq;
         euf::sgraph&                  m_sg;
         region                        m_region;
@@ -815,9 +814,11 @@ namespace seq {
         nielsen_graph(euf::sgraph& sg, simple_solver& solver);
         ~nielsen_graph();
 
+        ast_manager &get_manager() {
+            return m;
+        }
+        
         euf::sgraph& sg() { return m_sg; }
-        ast_manager& m() { return m_m; }
-        ast_manager const& m() const { return m_m; }
         seq_util& seq() { return m_seq; }
         seq_util const& seq() const { return m_seq; }
 
diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp
index 70f8eeb1c..b5d994291 100644
--- a/src/smt/seq/seq_regex.cpp
+++ b/src/smt/seq/seq_regex.cpp
@@ -770,7 +770,7 @@ namespace seq {
                 new_history = m_sg.mk(chain);
             }
         }
-        return seq::str_mem(mem.m_str, mem.m_regex, mem.m_lit, new_history, mem.m_id, mem.m_dep);
+        return seq::str_mem(mem.m_str, mem.m_regex, new_history, mem.m_id, mem.m_dep);
     }
 
     // -----------------------------------------------------------------------
diff --git a/src/smt/seq/seq_regex.h b/src/smt/seq/seq_regex.h
index 662478d2d..5c3bf2843 100644
--- a/src/smt/seq/seq_regex.h
+++ b/src/smt/seq/seq_regex.h
@@ -246,7 +246,7 @@ namespace seq {
             if (deriv)
                 propagate_self_stabilizing(parent_re, deriv);
             euf::snode* new_str = m_sg.drop_first(mem.m_str);
-            return seq::str_mem(new_str, deriv, mem.m_lit, mem.m_history, mem.m_id, mem.m_dep);
+            return seq::str_mem(new_str, deriv, mem.m_history, mem.m_id, mem.m_dep);
         }
 
         // -----------------------------------------------------------------
diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h
index 2ba99ad78..b083f56dd 100644
--- a/src/smt/seq/seq_state.h
+++ b/src/smt/seq/seq_state.h
@@ -27,6 +27,18 @@ namespace smt {
 
     class enode;
 
+    struct tracked_str_eq : public seq::str_eq {
+        enode *m_l, *m_r;
+        tracked_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep)
+            : seq::str_eq(lhs, rhs, dep), m_l(l), m_r(r) {}
+    };
+
+    struct tracked_str_mem : public seq::str_mem {
+        sat::literal lit;
+        tracked_str_mem(euf::snode *str, euf::snode *regex, sat::literal lit, euf::snode *history, unsigned id, seq::dep_tracker const &dep)
+            : seq::str_mem(str, regex, history, id, dep), lit(lit) {}
+    };
+
     // source info for a string disequality
     struct diseq_source {
         enode* m_n1;
@@ -34,8 +46,8 @@ namespace smt {
     };
 
     class seq_state {
-        vector<seq::str_eq>     m_str_eqs;
-        vector<seq::str_mem>    m_str_mems;
+        vector<tracked_str_eq>     m_str_eqs;
+        vector<tracked_str_mem>    m_str_mems;
         vector<diseq_source>    m_diseqs;
         unsigned_vector         m_str_eq_lim;
         unsigned_vector         m_str_mem_lim;
@@ -64,20 +76,20 @@ namespace smt {
 
         void add_str_eq(euf::snode* lhs, euf::snode* rhs, enode* n1, enode* n2) {
             seq::dep_tracker dep = nullptr;
-            m_str_eqs.push_back(seq::str_eq(lhs, rhs, n1, n2, dep));
+            m_str_eqs.push_back(tracked_str_eq(lhs, rhs, n1, n2, dep));
         }
 
         void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) {
             seq::dep_tracker dep = nullptr;
-            m_str_mems.push_back(seq::str_mem(str, regex, lit, nullptr, m_next_mem_id++, dep));
+            m_str_mems.push_back(tracked_str_mem(str, regex, lit, nullptr, m_next_mem_id++, dep));
         }
 
         void add_diseq(enode* n1, enode* n2) {
             m_diseqs.push_back({n1, n2});
         }
 
-        vector<seq::str_eq> const&  str_eqs()  const { return m_str_eqs; }
-        vector<seq::str_mem> const& str_mems() const { return m_str_mems; }
+        vector<tracked_str_eq> const&  str_eqs()  const { return m_str_eqs; }
+        vector<tracked_str_mem> const& str_mems() const { return m_str_mems; }
         vector<diseq_source> const& diseqs()   const { return m_diseqs; }
 
         diseq_source const& get_diseq(unsigned i) const { return m_diseqs[i]; }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index a339abd7b..da3e20ac7 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -282,7 +282,7 @@ namespace smt {
         if (m_regex.is_empty_regex(mem.m_regex)) {
             enode_pair_vector eqs;
             literal_vector lits;
-            lits.push_back(mem.m_lit);
+            lits.push_back(mem.lit);
             set_conflict(eqs, lits);
             return;
         }
@@ -291,7 +291,7 @@ namespace smt {
         if (mem.m_str->is_empty() && !mem.m_regex->is_nullable()) {
             enode_pair_vector eqs;
             literal_vector lits;
-            lits.push_back(mem.m_lit);
+            lits.push_back(mem.lit);
             set_conflict(eqs, lits);
             return;
         }
@@ -330,18 +330,18 @@ namespace smt {
                 continue;  // trivially satisfied, skip
             if (triv < 0) {
                 // trivially unsat: add anyway so solve() detects conflict
-                m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.m_lit);
+                m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.lit);
                 continue;
             }
             // pre-process: consume ground prefix characters
             vector<seq::str_mem> processed;
             if (!m_regex.process_str_mem(mem, processed)) {
                 // conflict during ground prefix consumption
-                m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.m_lit);
+                m_nielsen.add_str_mem(mem.m_str, mem.m_regex, mem.lit);
                 continue;
             }
             for (auto const& pm : processed) {
-                m_nielsen.add_str_mem(pm.m_str, pm.m_regex, pm.m_lit);
+                m_nielsen.add_str_mem(pm.m_str, pm.m_regex, mem.lit);
             }
         }
 
@@ -839,9 +839,9 @@ namespace smt {
                 literal_vector lits;
                 for (unsigned i : mem_indices) {
                     auto const &src = m_state.str_mems()[i];
-                    SASSERT(ctx.get_assignment(src.m_lit) == l_true); // we already stored the polarity of the literal
+                    SASSERT(ctx.get_assignment(src.lit) == l_true); // we already stored the polarity of the literal
                     lits.push_back(
-                        src.m_lit);
+                        src.lit);
                 }
                 TRACE(seq, tout << "nseq regex precheck: empty intersection for var "
                                 << var_id << ", conflict with " << lits.size() << " lits\n";);