diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index a8774de8e..c9c81a02f 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -73,6 +73,9 @@ namespace euf {
         if (m_seq.re.is_star(e))
             return snode_kind::s_star;
 
+        if (m_seq.re.is_plus(e))
+            return snode_kind::s_plus;
+
         if (m_seq.re.is_loop(e))
             return snode_kind::s_loop;
 
@@ -172,6 +175,7 @@ namespace euf {
         }
 
         case snode_kind::s_star:
+        case snode_kind::s_plus:
             SASSERT(n->num_args() == 1);
             n->m_ground = n->arg(0)->is_ground();
             n->m_regex_free = false;
@@ -759,6 +763,7 @@ namespace euf {
             case snode_kind::s_concat:     return "concat";
             case snode_kind::s_power:      return "power";
             case snode_kind::s_star:       return "star";
+            case snode_kind::s_plus:       return "plus";
             case snode_kind::s_loop:       return "loop";
             case snode_kind::s_union:      return "union";
             case snode_kind::s_intersect:  return "intersect";
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index 8ca8cac67..1493b4a94 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -45,6 +45,7 @@ namespace euf {
         s_concat,      // concatenation of two snodes (OP_SEQ_CONCAT)
         s_power,       // string exponentiation s^n (OP_SEQ_POWER)
         s_star,        // Kleene star r* (OP_RE_STAR)
+        s_plus,        // Kleene plus  r+ (OP_RE_PLUS)
         s_loop,        // bounded loop r{lo,hi} (OP_RE_LOOP)
         s_union,       // union r1|r2 (OP_RE_UNION)
         s_intersect,   // intersection r1&r2 (OP_RE_INTERSECT)
@@ -165,6 +166,9 @@ namespace euf {
         bool is_star() const {
             return m_kind == snode_kind::s_star;
         }
+        bool is_plus() const {
+            return m_kind == snode_kind::s_plus;
+        }
         bool is_loop() const {
             return m_kind == snode_kind::s_loop;
         }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 683910462..adef5b26d 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -613,8 +613,8 @@ namespace smt {
                     ++num_mems;
                     continue;
                 }
-                /*if (m_ignored_mem.contains(mem.lit))
-                    continue; // already handled via Boolean closure, skip*/
+                if (m_ignored_mem.contains(mem.lit))
+                    continue; // already handled via Boolean closure, skip
                 // pre-process: consume ground prefix characters
                 vector<seq::str_mem> processed;
                 if (!m_regex.process_str_mem(mem, processed)) {
@@ -753,31 +753,31 @@ namespace smt {
                 m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh);
                 m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
                 m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
+            }
 
-                SASSERT(!m_nielsen.root()->is_currently_conflict());
+            SASSERT(!m_nielsen.root()->is_currently_conflict());
 
-                // Regex membership pre-check: before running DFS, check intersection
-                // emptiness for each variable's regex constraints.  This handles
-                // regex-only problems that the DFS cannot efficiently solve.
-                if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) {
-                    switch (check_regex_memberships_precheck()) {
-                    case l_true:
-                        // conflict was asserted inside check_regex_memberships_precheck
-                        TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n");
+            // Regex membership pre-check: before running DFS, check intersection
+            // emptiness for each variable's regex constraints.  This handles
+            // regex-only problems that the DFS cannot efficiently solve.
+            if (!m_nielsen.root()->is_currently_conflict() && get_fparams().m_nseq_regex_precheck) {
+                switch (check_regex_memberships_precheck()) {
+                case l_true:
+                    // conflict was asserted inside check_regex_memberships_precheck
+                    TRACE(seq, tout << "nseq final_check: regex precheck UNSAT\n");
+                    return FC_CONTINUE;
+                case l_false:
+                    // all regex constraints satisfiable, no word eqs → SAT
+                    TRACE(seq, tout << "nseq final_check: regex precheck SAT\n");
+                    m_nielsen.set_sat_node(m_nielsen.root());
+                    if (!check_length_coherence())
                         return FC_CONTINUE;
-                    case l_false:
-                        // all regex constraints satisfiable, no word eqs → SAT
-                        TRACE(seq, tout << "nseq final_check: regex precheck SAT\n");
-                        m_nielsen.set_sat_node(m_nielsen.root());
-                        if (!check_length_coherence())
-                            return FC_CONTINUE;
-                        if (!check_stoi_coherence())
-                            return FC_CONTINUE;
-                        TRACE(seq, tout << "pre-check done\n");
-                        return FC_DONE;
-                    default:
-                        break;
-                    }
+                    if (!check_stoi_coherence())
+                        return FC_CONTINUE;
+                    TRACE(seq, tout << "pre-check done\n");
+                    return FC_DONE;
+                default:
+                    break;
                 }
             }
 
@@ -1659,6 +1659,7 @@ namespace smt {
 
     bool theory_nseq::check_length_coherence() {
         if (m_relevant_lengths.empty())
+            // TODO: Make use of this; so far we always introduce lengths always
             return true;
 
         SASSERT(m_nielsen.sat_node());