diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 6fc1e5eff..4d534a1d4 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -443,8 +443,7 @@ namespace smt {
 
     void theory_nseq::propagate_pos_mem(tracked_str_mem const& mem) {
 
-        if (!mem.m_str || !mem.m_regex)
-            return;
+        SASSERT(mem.well_formed());
 
         // regex is ∅ → conflict
         if (m_regex.is_empty_regex(mem.m_regex)) {
@@ -1380,7 +1379,7 @@ namespace smt {
 
         for (unsigned i = 0; i < mems.size(); ++i) {
             auto const& mem = *mems[i];
-            SASSERT(mem.m_str && mem.m_regex);
+            SASSERT(mem.well_formed());
             if (mem.is_primitive()) {
                 auto& vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector());
                 vec.push_back(i);
@@ -1393,21 +1392,18 @@ namespace smt {
             return l_undef;
 
         // Check if there are any eq items in the queue (needed for SAT condition below).
-        bool has_eqs = false;
-        for (auto const& item : m_prop_queue)
-            if (std::holds_alternative<eq_item>(item)) { has_eqs = true; break; }
+        bool has_eqs = any_of(m_prop_queue, [](auto p) { return std::holds_alternative<eq_item>(p); });
 
         bool any_undef = false;
 
         // Check intersection emptiness for each variable.
-        for (auto& kv : var_to_mems) {
-            unsigned var_id = kv.m_key;
-            unsigned_vector const& mem_indices = kv.m_value;
+        for (auto &[var_id, mem_indices] : var_to_mems) {
+
             ptr_vector<euf::snode> regexes;
             for (unsigned i : mem_indices) {
                 euf::snode* re = mems[i]->m_regex;
-                if (re)
-                    regexes.push_back(re);
+                SASSERT(re);
+                regexes.push_back(re);
             }
             if (regexes.empty())
                 continue;
@@ -1463,7 +1459,8 @@ namespace smt {
         u_map<unsigned_vector> var_to_mems;
         for (unsigned i = 0; i < mems.size(); ++i) {
             auto const &mem = mems[i];
-            if (mem.is_primitive() && mem.m_str) {
+            SASSERT(mem.well_formed());
+            if (mem.is_primitive()) {
                 auto &vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector());
                 vec.push_back(i);
             }
@@ -1494,10 +1491,9 @@ namespace smt {
 
             unsigned_vector const &mem_indices = var_to_mems[var_id];
             ptr_vector<euf::snode> regexes;
-            for (const unsigned i : mem_indices) {
-                euf::snode *re = mems[i].m_regex;
-                if (re)
-                    regexes.push_back(re);
+            for (auto i : mem_indices) {
+                SASSERT(mems[i].well_formed());
+                regexes.push_back(mems[i].m_regex);
             }
 
             SASSERT(!regexes.empty());
diff --git a/src/test/euf_seq_plugin.cpp b/src/test/euf_seq_plugin.cpp
index 4beaa012e..877eb5f94 100644
--- a/src/test/euf_seq_plugin.cpp
+++ b/src/test/euf_seq_plugin.cpp
@@ -46,14 +46,12 @@ static void test_sgraph_basic() {
     SASSERT(sx->is_var());
     SASSERT(!sx->is_ground());
     SASSERT(sx->is_regex_free());
-    SASSERT(!sx->is_nullable());
     SASSERT(sx->length() == 1);
 
     euf::snode* se = sg.mk(empty);
     SASSERT(se);
     SASSERT(se->is_empty());
     SASSERT(se->is_ground());
-    SASSERT(se->is_nullable());
     SASSERT(se->length() == 0);
 
     euf::snode* sxy = sg.mk(xy);
@@ -172,7 +170,6 @@ static void test_seq_plugin_star_merge() {
     sg.mk(star_star);
     euf::snode* s = sg.find(star_x);
     SASSERT(s && s->is_star());
-    SASSERT(s->is_nullable());
 
     std::cout << g << "\n";
 }
diff --git a/src/test/euf_sgraph.cpp b/src/test/euf_sgraph.cpp
index d4251c53b..311fe254a 100644
--- a/src/test/euf_sgraph.cpp
+++ b/src/test/euf_sgraph.cpp
@@ -38,7 +38,6 @@ static void test_sgraph_classify() {
     SASSERT(sx && sx->is_var());
     SASSERT(!sx->is_ground());
     SASSERT(sx->is_regex_free());
-    SASSERT(!sx->is_nullable());
     SASSERT(sx->level() == 1);
     SASSERT(sx->length() == 1);
     SASSERT(sx->is_token());
@@ -48,7 +47,6 @@ static void test_sgraph_classify() {
     euf::snode* se = sg.mk(empty);
     SASSERT(se && se->is_empty());
     SASSERT(se->is_ground());
-    SASSERT(se->is_nullable());
     SASSERT(se->level() == 0);
     SASSERT(se->length() == 0);
     SASSERT(!se->is_token());
@@ -59,7 +57,6 @@ static void test_sgraph_classify() {
     euf::snode* sca = sg.mk(unit_a);
     SASSERT(sca && sca->is_char());
     SASSERT(sca->is_ground());
-    SASSERT(!sca->is_nullable());
     SASSERT(sca->level() == 1);
     SASSERT(sca->length() == 1);
     SASSERT(sca->is_token());
@@ -71,7 +68,6 @@ static void test_sgraph_classify() {
     SASSERT(sxy && sxy->is_concat());
     SASSERT(!sxy->is_ground());
     SASSERT(sxy->is_regex_free());
-    SASSERT(!sxy->is_nullable());
     SASSERT(sxy->level() == 2);
     SASSERT(sxy->length() == 2);
     SASSERT(sxy->num_args() == 2);
@@ -98,7 +94,6 @@ static void test_sgraph_regex() {
     euf::snode* str = sg.mk(to_re_x);
     SASSERT(str && str->is_to_re());
     SASSERT(!str->is_regex_free());
-    SASSERT(!str->is_nullable()); // to_re(x) nullable iff x nullable, x is var so not nullable
     SASSERT(str->num_args() == 1);
 
     // star
@@ -106,7 +101,6 @@ static void test_sgraph_regex() {
     euf::snode* ss = sg.mk(star_x);
     SASSERT(ss && ss->is_star());
     SASSERT(!ss->is_regex_free());
-    SASSERT(ss->is_nullable()); // star is always nullable
     SASSERT(ss->num_args() == 1);
 
     // full_seq (.*)
@@ -114,39 +108,33 @@ static void test_sgraph_regex() {
     euf::snode* sfs = sg.mk(full_seq);
     SASSERT(sfs && sfs->is_full_seq());
     SASSERT(sfs->is_ground());
-    SASSERT(sfs->is_nullable());
 
     // full_char (.)
     expr_ref full_char(seq.re.mk_full_char(str_sort), m);
     euf::snode* sfc = sg.mk(full_char);
     SASSERT(sfc && sfc->is_full_char());
     SASSERT(sfc->is_ground());
-    SASSERT(!sfc->is_nullable());
 
     // empty set, fail
     sort_ref re_sort(seq.re.mk_re(str_sort), m);
     expr_ref empty_set(seq.re.mk_empty(re_sort), m);
     euf::snode* sfail = sg.mk(empty_set);
     SASSERT(sfail && sfail->is_fail());
-    SASSERT(!sfail->is_nullable());
 
     // union: to_re(x) | star(to_re(x)), nullable because star is
     expr_ref re_union(seq.re.mk_union(to_re_x, star_x), m);
     euf::snode* su = sg.mk(re_union);
     SASSERT(su && su->is_union());
-    SASSERT(su->is_nullable()); // star_x is nullable
 
     // intersection: to_re(x) & star(to_re(x)), nullable only if both are
     expr_ref re_inter(seq.re.mk_inter(to_re_x, star_x), m);
     euf::snode* si = sg.mk(re_inter);
     SASSERT(si && si->is_intersect());
-    SASSERT(!si->is_nullable()); // to_re(x) is not nullable
 
     // complement of to_re(x): nullable because to_re(x) is not nullable
     expr_ref re_comp(seq.re.mk_complement(to_re_x), m);
     euf::snode* sc = sg.mk(re_comp);
     SASSERT(sc && sc->is_complement());
-    SASSERT(sc->is_nullable()); // complement of non-nullable is nullable
 
     // in_re
     expr_ref in_re(seq.re.mk_in_re(x, star_x), m);
@@ -176,7 +164,6 @@ static void test_sgraph_power() {
     SASSERT(sp && sp->is_power());
     SASSERT(!sp->is_ground()); // base x is not ground
     SASSERT(sp->is_regex_free());
-    SASSERT(!sp->is_nullable()); // base x is not nullable
     SASSERT(sp->num_args() >= 1);
 
     sg.display(std::cout);
@@ -400,14 +387,12 @@ static void test_sgraph_concat_metadata() {
     euf::snode* sxz = sg.mk(xz);
     SASSERT(!sxz->is_ground());
     SASSERT(sxz->is_regex_free());
-    SASSERT(!sxz->is_nullable());
     SASSERT(sxz->length() == 2);
     SASSERT(sxz->level() == 2);
 
     // concat(empty, empty): nullable (both empty)
     expr_ref empty2(seq.str.mk_concat(empty, empty), m);
     euf::snode* see = sg.mk(empty2);
-    SASSERT(see->is_nullable());
     SASSERT(see->is_ground());
     SASSERT(see->length() == 0);
 
@@ -466,7 +451,6 @@ static void test_sgraph_factory() {
     // mk_empty
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
     SASSERT(e && e->is_empty());
-    SASSERT(e->is_nullable());
     SASSERT(e->length() == 0);
 
     // mk_concat with empty absorption
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index c4aedffe5..d0f84bc4a 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -127,7 +127,7 @@ static void test_str_mem() {
     euf::snode* regex = sg.mk(star_fc);
 
     seq::dep_tracker dep = nullptr;
-    seq::str_mem mem(x, regex, e, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     // x in regex is primitive (x is a single variable)
     SASSERT(mem.is_primitive());
@@ -136,7 +136,7 @@ static void test_str_mem() {
     // concatenation is not primitive
     euf::snode* a = sg.mk_char('A');
     euf::snode* xa = sg.mk_concat(x, a);
-    seq::str_mem mem2(xa, regex, e, 1, dep);
+    seq::str_mem mem2(xa, regex, dep);
     SASSERT(!mem2.is_primitive());
     SASSERT(mem2.contains_var(x));
 }
@@ -280,7 +280,6 @@ static void test_nielsen_graph_populate() {
     euf::snode* regex = sg.mk(re_all);
     ng.add_str_mem(x, regex);
     SASSERT(ng.root()->str_mems().size() == 1);
-    SASSERT(ng.root()->str_mems()[0].m_id == 0);
 
     // add another equality: concat(x, A) = concat(A, y)
     euf::snode* xa = sg.mk_concat(x, a);
@@ -456,8 +455,6 @@ static void test_multiple_memberships() {
 
     SASSERT(ng.root() != nullptr);
     SASSERT(ng.root()->str_mems().size() == 2);
-    SASSERT(ng.root()->str_mems()[0].m_id == 0);
-    SASSERT(ng.root()->str_mems()[1].m_id == 1);
 
     ng.display(std::cout);
 }
@@ -1866,7 +1863,7 @@ static void test_simplify_regex_infeasible() {
     // ε ∈ to_re("A") → non-nullable → conflict
     seq::nielsen_node* node = ng.mk_node();
     seq::dep_tracker dep = nullptr;
-    node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
+    node->add_str_mem(seq::str_mem(e, regex, dep));
 
     auto sr = node->simplify_and_init({});
     SASSERT(sr == seq::simplify_result::conflict);
@@ -1922,7 +1919,7 @@ static void test_simplify_brzozowski_sat() {
     // "A" ∈ to_re("A") → derivative consumes 'A' → ε ∈ ε-regex → satisfied
     seq::nielsen_node* node = ng.mk_node();
     seq::dep_tracker dep = nullptr;
-    node->add_str_mem(seq::str_mem(a, regex, e, 0, dep));
+    node->add_str_mem(seq::str_mem(a, regex, dep));
 
     auto sr = node->simplify_and_init({});
     SASSERT(sr == seq::simplify_result::satisfied);
@@ -1954,7 +1951,7 @@ static void test_simplify_brzozowski_rtl_suffix() {
     // x·"A" ∈ to_re("BA") → RTL consume trailing 'A' → x ∈ to_re("B")
     seq::nielsen_node* node = ng.mk_node();
     seq::dep_tracker dep = nullptr;
-    node->add_str_mem(seq::str_mem(xa, regex, e, 0, dep));
+    node->add_str_mem(seq::str_mem(xa, regex, dep));
 
     auto sr = node->simplify_and_init({});
     SASSERT(sr == seq::simplify_result::proceed);
@@ -3294,7 +3291,8 @@ static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::sno
 
 static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {
     rational lb;
-    if (!node->lower_bound(var->get_expr(), lb))
+    seq::dep_tracker d = nullptr;
+    if (!node->lower_bound(var->get_expr(), lb, d))
         return 0;
     SASSERT(lb.is_unsigned());
     return lb.is_unsigned() ? lb.get_unsigned() : 0;
@@ -3302,7 +3300,8 @@ static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {
 
 static unsigned queried_ub(seq::nielsen_node* node, euf::snode* var) {
     rational ub;
-    if (!node->upper_bound(var->get_expr(), ub))
+    seq::dep_tracker d = nullptr;
+    if (!node->upper_bound(var->get_expr(), ub, d))
         return UINT_MAX;
     SASSERT(ub.is_unsigned());
     return ub.is_unsigned() ? ub.get_unsigned() : UINT_MAX;
diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp
index e4cd17088..6d4ad4cfd 100644
--- a/src/test/seq_parikh.cpp
+++ b/src/test/seq_parikh.cpp
@@ -324,7 +324,7 @@ static void test_generate_constraints_ab_star() {
     seq::dep_manager dm;
     sat::literal lit = sat::null_literal;  // dummy literal for dependency tracking 
     seq::dep_tracker dep = dm.mk_leaf(lit);
-    seq::str_mem mem(x, regex, nullptr, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
@@ -371,7 +371,7 @@ static void test_generate_constraints_bounded_loop() {
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
-    seq::str_mem mem(x, regex, nullptr, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
@@ -408,7 +408,7 @@ static void test_generate_constraints_stride_one() {
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
-    seq::str_mem mem(x, regex, nullptr, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
@@ -431,7 +431,7 @@ static void test_generate_constraints_fixed_length() {
     euf::snode* regex = sg.mk(re);
     seq::dep_manager dm;
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
-    seq::str_mem mem(x, regex, nullptr, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
@@ -455,7 +455,7 @@ static void test_generate_constraints_dep_propagated() {
     seq::dep_manager dm;
     sat::literal lit(7);
     seq::dep_tracker dep = dm.mk_leaf(lit);
-    seq::str_mem mem(x, regex, nullptr, 0, dep);
+    seq::str_mem mem(x, regex, dep);
 
     vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);