diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 84041b381..7765a3e2e 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -32,9 +32,6 @@ NSB review:
 #include "ast/ast_pp.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/th_rewriter.h"
-#include "sat/smt/arith_solver.h"
-#include "tactic/probe.h"
-#include "tactic/fd_solver/enum2bv_solver.h"
 #include "util/hashtable.h"
 #include "util/statistics.h"
 #include <algorithm>
@@ -203,14 +200,14 @@ namespace seq {
     void nielsen_node::clone_from(nielsen_node const& parent) {
         m_str_eq.reset();
         m_str_mem.reset();
-        m_int_constraints.reset();
+        m_constraints.reset();
         m_char_diseqs.reset();
         m_char_ranges.reset();
         m_var_lb.reset();
         m_var_ub.reset();
         m_str_eq.append(parent.m_str_eq);
         m_str_mem.append(parent.m_str_mem);
-        m_int_constraints.append(parent.m_int_constraints);
+        m_constraints.append(parent.m_constraints);
         
         // clone character disequalities
         
@@ -336,13 +333,13 @@ namespace seq {
             m_reason = backtrack_reason::arithmetic;
             return true;
         }
-        // add int_constraint: len(var) >= lb
+        // add constraint: len(var) >= lb
         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);
         expr_ref bound(arith.mk_int(lb), m);
-        m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::ge, dep, m));
+        m_constraints.push_back(constraint(arith.mk_ge(len_var, bound), dep, m));
         return true;
     }
 
@@ -362,13 +359,13 @@ namespace seq {
             m_reason = backtrack_reason::arithmetic;
             return true;
         }
-        // add int_constraint: len(var) <= ub
+        // add constraint: len(var) <= ub
         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);
         expr_ref bound(arith.mk_int(ub), m);
-        m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::le, dep, m));
+        m_constraints.push_back(constraint(arith.mk_le(len_var, bound), dep, m));
         return true;
     }
 
@@ -466,19 +463,19 @@ namespace seq {
                     add_upper_int_bound(mem.m_str, max_len, mem.m_dep);
             }
             else {
-                // str is a concatenation or other term: add as general int_constraints
+                // str is a concatenation or other term: add as general constraints
                 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) {
                     expr_ref bound(arith.mk_int(min_len), m);
-                    m_int_constraints.push_back(
-                        int_constraint(len_str, bound, int_constraint_kind::ge, mem.m_dep, m));
+                    m_constraints.push_back(
+                        constraint(arith.mk_ge(len_str, bound), mem.m_dep, m));
                 }
                 if (max_len < UINT_MAX) {
                     expr_ref bound(arith.mk_int(max_len), m);
-                    m_int_constraints.push_back(
-                        int_constraint(len_str, bound, int_constraint_kind::le, mem.m_dep, m));
+                    m_constraints.push_back(
+                        constraint(arith.mk_le(len_str, bound), mem.m_dep, m));
                 }
             }
         }
@@ -566,7 +563,7 @@ namespace seq {
     nielsen_node* nielsen_graph::mk_child(nielsen_node* parent) {
         nielsen_node* child = mk_node();
         child->clone_from(*parent);
-        child->m_parent_ic_count = parent->int_constraints().size();
+        child->m_parent_ic_count = parent->constraints().size();
         return child;
     }
 
@@ -597,7 +594,7 @@ namespace seq {
 
     // test-friendly overloads (no external dependency tracking)
     void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
-        if (root())
+        if (!root())
             create_root();
         dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
         str_eq eq(lhs, rhs, dep);
@@ -679,8 +676,8 @@ namespace seq {
                 if (e) seq.str.is_power(e, pow_base, pow_exp);
                 if (pow_exp) {
                     expr* zero = arith.mk_numeral(rational(0), true);
-                    m_int_constraints.push_back(
-                        int_constraint(pow_exp, zero, int_constraint_kind::eq, dep, m));
+                    m_constraints.push_back(
+                        constraint(m.mk_eq(pow_exp, zero), dep, m));
                 }
                 nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep);
                 apply_subst(sg, s);
@@ -974,7 +971,8 @@ namespace seq {
         return {expr_ref(last_stable_sum, m), last_stable_idx};
     }
 
-    simplify_result nielsen_node::simplify_and_init(svector<nielsen_edge*> const& cur_path) {
+    simplify_result nielsen_node::simplify_and_init() {
+        svector<nielsen_edge*> const& cur_path = m_graph.cur_path();
         if (m_is_extended)
             return simplify_result::proceed;
 
@@ -1142,8 +1140,8 @@ namespace seq {
                             pow_le_count = diff.is_nonneg();
                         }
                         else if (!cur_path.empty()) {
-                            pow_le_count = m_graph.check_lp_le(pow_exp, norm_count, this, cur_path);
-                            count_le_pow = m_graph.check_lp_le(norm_count, pow_exp, this, cur_path);
+                            pow_le_count = m_graph.check_lp_le(pow_exp, norm_count, this);
+                            count_le_pow = m_graph.check_lp_le(norm_count, pow_exp, this);
                         }
                         if (!pow_le_count && !count_le_pow)
                             continue;
@@ -1219,8 +1217,8 @@ namespace seq {
                     }
                     // 3e: LP-aware power directional elimination
                     else if (lp && rp && !cur_path.empty()) {
-                        bool lp_le_rp = m_graph.check_lp_le(lp, rp, this, cur_path);
-                        bool rp_le_lp = m_graph.check_lp_le(rp, lp, this, cur_path);
+                        bool lp_le_rp = m_graph.check_lp_le(lp, rp, this);
+                        bool rp_le_lp = m_graph.check_lp_le(rp, lp, this);
                         if (lp_le_rp || rp_le_lp) {
                             expr* smaller_exp = lp_le_rp ? lp : rp;
                             expr* larger_exp  = lp_le_rp ? rp : lp;
@@ -1228,15 +1226,15 @@ namespace seq {
                             eq.m_rhs = dir_drop(sg, eq.m_rhs, 1, fwd);
                             if (lp_le_rp && rp_le_lp) {
                                 // both ≤ -> equal -> both cancel completely
-                                add_int_constraint(m_graph.mk_int_constraint(lp, rp, int_constraint_kind::eq, eq.m_dep));
+                                add_constraint(m_graph.mk_constraint(m.mk_eq(lp, rp), eq.m_dep));
                             }
                             else {
                                 // strictly less: create diff power d = larger - smaller >= 1
                                 expr_ref d(m_graph.mk_fresh_int_var());
                                 expr_ref one_e(arith.mk_int(1), m);
                                 expr_ref d_plus_smaller(arith.mk_add(d, smaller_exp), m);
-                                add_int_constraint(m_graph.mk_int_constraint(d, one_e, int_constraint_kind::ge, eq.m_dep));
-                                add_int_constraint(m_graph.mk_int_constraint(d_plus_smaller, larger_exp, int_constraint_kind::eq, eq.m_dep));
+                                add_constraint(m_graph.mk_constraint(arith.mk_ge(d, one_e), eq.m_dep));
+                                add_constraint(m_graph.mk_constraint(m.mk_eq(d_plus_smaller, larger_exp), eq.m_dep));
                                 expr_ref pw(seq.str.mk_power(lb, d), m);
                                 euf::snode*& larger_side = lp_le_rp ? eq.m_rhs : eq.m_lhs;
                                 larger_side = dir_concat(sg, sg.mk(pw), larger_side, fwd);
@@ -1371,7 +1369,7 @@ namespace seq {
         }
 
         // IntBounds initialization: derive per-variable Parikh length bounds from
-        // remaining regex memberships and add to m_int_constraints.
+        // remaining regex memberships and add to constraints.
         init_var_bounds_from_mems();
 
         if (is_satisfied())
@@ -1503,8 +1501,8 @@ namespace seq {
                 if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth)
                     break;
                 inc_run_idx();
-                svector<nielsen_edge *> cur_path;
-                search_result r = search_dfs(m_root, 0, cur_path);
+                m_cur_path.reset();
+                search_result r = search_dfs(m_root, 0);
                 IF_VERBOSE(1, verbose_stream()
                                   << " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes
                                   << " max_depth=" << m_stats.m_max_depth << " extensions=" << m_stats.m_num_extensions
@@ -1536,7 +1534,7 @@ namespace seq {
         }
     }
 
-    nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path) {
+    nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node, unsigned depth) {
         ++m_stats.m_num_dfs_nodes;
         m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
 
@@ -1553,7 +1551,7 @@ namespace seq {
         if (node->eval_idx() == m_run_idx) {
             if (node->is_satisfied()) {
                 m_sat_node = node;
-                m_sat_path = cur_path;
+                m_sat_path = m_cur_path;
                 return search_result::sat;
             }
             if (node->is_currently_conflict())
@@ -1563,7 +1561,7 @@ namespace seq {
         node->set_eval_idx(m_run_idx);
 
         // simplify constraints (idempotent after first call)
-        simplify_result sr = node->simplify_and_init(cur_path);
+        simplify_result sr = node->simplify_and_init();
 
         if (sr == simplify_result::conflict) {
             ++m_stats.m_num_simplify_conflict;
@@ -1593,7 +1591,7 @@ namespace seq {
 
         // integer feasibility check: the solver now holds all path constraints
         // incrementally; just query the solver directly
-        if (!cur_path.empty() && !check_int_feasibility(node, cur_path)) {
+        if (!m_cur_path.empty() && !check_int_feasibility(node)) {
             node->set_reason(backtrack_reason::arithmetic);
             ++m_stats.m_num_arith_infeasible;
             return search_result::unsat;
@@ -1610,7 +1608,7 @@ namespace seq {
                 return search_result::unsat;
             }
             m_sat_node = node;
-            m_sat_path = cur_path;
+            m_sat_path = m_cur_path;
             return search_result::sat;
         }
 
@@ -1636,15 +1634,15 @@ namespace seq {
         // explore children
         bool any_unknown = false;
         for (nielsen_edge *e : node->outgoing()) {
-            cur_path.push_back(e);
+            m_cur_path.push_back(e);
             // Push a solver scope for this edge and assert its side integer
-            // constraints.  The child's own new int_constraints will be asserted
+            // constraints.  The child's own new constraints will be asserted
             // inside the recursive call (above).  On return, pop the scope so
             // that backtracking removes those assertions.
             m_solver.push();
 
             // Lazily compute substitution length constraints (|x| = |u|) on first
-            // traversal. This must happen before asserting side_int and before
+            // traversal. This must happen before asserting side_constraints and before
             // bumping mod counts, so that LHS uses the parent's counts and RHS
             // uses the temporarily-bumped counts.
             if (!e->len_constraints_computed()) {
@@ -1652,14 +1650,13 @@ namespace seq {
                 e->set_len_constraints_computed(true);
             }
 
-            for (auto const &ic : e->side_int()) {
-                m_solver.assert_expr(int_constraint_to_expr(ic));
-            }
+            for (auto const &ic : e->side_constraints())
+                m_solver.assert_expr(ic.fml);
 
             // Bump modification counts for the child's context.
             inc_edge_mod_counts(e);
 
-            search_result r = search_dfs(e->tgt(), e->is_progress() ? depth : depth + 1, cur_path);
+            search_result r = search_dfs(e->tgt(), e->is_progress() ? depth : depth + 1);
 
             // Restore modification counts on backtrack.
             dec_edge_mod_counts(e);
@@ -1667,7 +1664,7 @@ namespace seq {
             m_solver.pop(1);
             if (r == search_result::sat)
                 return search_result::sat;
-            cur_path.pop_back();
+            m_cur_path.pop_back();
             if (r == search_result::unknown)
                 any_unknown = true;
         }
@@ -1808,8 +1805,7 @@ namespace seq {
                     expr* pow_exp = get_power_exp_expr(pow_head, seq);
                     if (pow_exp) {
                         expr* zero = arith.mk_numeral(rational(0), true);
-                        e->add_side_int(mk_int_constraint(
-                            pow_exp, zero, int_constraint_kind::eq, eq.m_dep));
+                        e->add_side_constraint(mk_constraint(m.mk_eq(pow_exp, zero), eq.m_dep));
                     }
                     return true;
                 }
@@ -2344,17 +2340,17 @@ namespace seq {
             if (pad && pad->get_expr()) {
                 expr_ref len_pad(seq.str.mk_length(pad->get_expr()), m);
                 expr_ref abs_pad(arith.mk_int(std::abs(padding)), m);
-                e->add_side_int(mk_int_constraint(len_pad, abs_pad, int_constraint_kind::eq, eq.m_dep));
+                e->add_side_constraint(mk_constraint(m.mk_eq(len_pad, abs_pad), eq.m_dep));
             }
             // 2) len(eq1_lhs) = len(eq1_rhs)
             expr_ref l1 = compute_length_expr(eq1_lhs);
             expr_ref r1 = compute_length_expr(eq1_rhs);
-            e->add_side_int(mk_int_constraint(l1, r1, int_constraint_kind::eq, eq.m_dep));
+            e->add_side_constraint(mk_constraint(m.mk_eq(l1, r1), eq.m_dep));
 
             // 3) len(eq2_lhs) = len(eq2_rhs)
             expr_ref l2 = compute_length_expr(eq2_lhs);
             expr_ref r2 = compute_length_expr(eq2_rhs);
-            e->add_side_int(mk_int_constraint(l2, r2, int_constraint_kind::eq, eq.m_dep));
+            e->add_side_constraint(mk_constraint(m.mk_eq(l2, r2), eq.m_dep));
 
             return true;
         }
@@ -2684,17 +2680,13 @@ namespace seq {
                     nielsen_node* child = mk_child(node);
                     nielsen_edge* e = mk_edge(node, child, true);
                     expr_ref n_plus_1(arith.mk_add(exp_n, arith.mk_int(1)), m);
-                    e->add_side_int(mk_int_constraint(
-                        exp_m, n_plus_1,
-                        int_constraint_kind::ge, eq.m_dep));
+                    e->add_side_constraint(mk_constraint(arith.mk_ge(exp_m, n_plus_1), eq.m_dep));
                 }
                 // Branch 2 (explored second): m <= n  (i.e., n >= m)
                 {
                     nielsen_node* child = mk_child(node);
                     nielsen_edge* e = mk_edge(node, child, true);
-                    e->add_side_int(mk_int_constraint(
-                        exp_n, exp_m,
-                        int_constraint_kind::ge, eq.m_dep));
+                    e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, exp_m), eq.m_dep));
                 }
                 return true;
             }
@@ -2758,17 +2750,13 @@ namespace seq {
                         nielsen_node* child = mk_child(node);
                         nielsen_edge* e = mk_edge(node, child, true);
                         expr_ref pow_plus1(arith.mk_add(pow_exp, arith.mk_int(1)), m);
-                        e->add_side_int(mk_int_constraint(
-                            norm_count, pow_plus1,
-                            int_constraint_kind::ge, eq.m_dep));
+                        e->add_side_constraint(mk_constraint(arith.mk_ge(norm_count, pow_plus1), eq.m_dep));
                     }
                     // Branch 2: count <= pow_exp (i.e., pow_exp >= count)
                     {
                         nielsen_node* child = mk_child(node);
                         nielsen_edge* e = mk_edge(node, child, true);
-                        e->add_side_int(mk_int_constraint(
-                            pow_exp, norm_count,
-                            int_constraint_kind::ge, eq.m_dep));
+                        e->add_side_constraint(mk_constraint(arith.mk_ge(pow_exp, norm_count), eq.m_dep));
                     }
                     return true;
                 }
@@ -2810,7 +2798,7 @@ namespace seq {
         e->add_subst(s1);
         child->apply_subst(m_sg, s1);
         if (exp_n)
-            e->add_side_int(mk_int_constraint(exp_n, zero, int_constraint_kind::eq, eq->m_dep));
+            e->add_side_constraint(mk_constraint(m.mk_eq(exp_n, zero), eq->m_dep));
 
         // Branch 2 (explored second): n >= 1 → peel one u: replace u^n with u · u^(n-1)
         // Side constraint: n >= 1
@@ -2834,7 +2822,7 @@ namespace seq {
         e->add_subst(s2);
         child->apply_subst(m_sg, s2);
         if (exp_n)
-            e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, eq->m_dep));
+            e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), eq->m_dep));
 
         return true;
     }
@@ -3137,15 +3125,15 @@ namespace seq {
             child->apply_subst(m_sg, s);
 
             // Side constraint: n >= 0
-            e->add_side_int(mk_int_constraint(fresh_n, zero, int_constraint_kind::ge, eq.m_dep));
+            e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_n, zero), eq.m_dep));
 
             // Side constraints for fresh partial exponent
             if (fresh_m.get()) {
                 expr* inner_exp = get_power_exponent(tok);
                 // m' >= 0
-                e->add_side_int(mk_int_constraint(fresh_m, zero, int_constraint_kind::ge, eq.m_dep));
+                e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_m, zero), eq.m_dep));
                 // m' <= inner_exp
-                e->add_side_int(mk_int_constraint(inner_exp, fresh_m, int_constraint_kind::ge, eq.m_dep));
+                e->add_side_constraint(mk_constraint(arith.mk_ge(inner_exp, fresh_m), eq.m_dep));
             }
         }
 
@@ -3479,18 +3467,18 @@ namespace seq {
                 child->apply_subst(m_sg, s);
 
                 // m >= 0
-                e->add_side_int(mk_int_constraint(fresh_m, zero, int_constraint_kind::ge, eq->m_dep));
+                e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_m, zero), eq->m_dep));
                 // m < n  ⟺  n >= m + 1
                 if (exp_n) {
                     expr_ref m_plus_1(arith.mk_add(fresh_m, arith.mk_int(1)), m);
-                    e->add_side_int(mk_int_constraint(exp_n, m_plus_1, int_constraint_kind::ge, eq->m_dep));
+                    e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, m_plus_1), eq->m_dep));
                 }
 
                 // Inner power constraints: 0 <= m' <= inner_exp
                 if (fresh_inner_m.get()) {
                     expr* inner_exp = get_power_exponent(tok);
-                    e->add_side_int(mk_int_constraint(fresh_inner_m, zero, int_constraint_kind::ge, eq->m_dep));
-                    e->add_side_int(mk_int_constraint(inner_exp, fresh_inner_m, int_constraint_kind::ge, eq->m_dep));
+                    e->add_side_constraint(mk_constraint(arith.mk_ge(fresh_inner_m, zero), eq->m_dep));
+                    e->add_side_constraint(mk_constraint(arith.mk_ge(inner_exp, fresh_inner_m), eq->m_dep));
                 }
             }
         }
@@ -3544,7 +3532,7 @@ namespace seq {
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             if (exp_n)
-                e->add_side_int(mk_int_constraint(exp_n, zero, int_constraint_kind::eq, eq->m_dep));
+                e->add_side_constraint(mk_constraint(m.mk_eq(exp_n, zero), eq->m_dep));
         }
 
         // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1)
@@ -3558,7 +3546,7 @@ namespace seq {
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             if (exp_n)
-                e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, eq->m_dep));
+                e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), eq->m_dep));
         }
 
         return true;
@@ -3589,7 +3577,7 @@ namespace seq {
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             if (exp_n)
-                e->add_side_int(mk_int_constraint(exp_n, zero, int_constraint_kind::eq, mem->m_dep));
+                e->add_side_constraint(mk_constraint(m.mk_eq(exp_n, zero), mem->m_dep));
         }
 
         // Branch 2: n >= 1 → peel one u: u^n → u · u^(n-1)
@@ -3603,7 +3591,7 @@ namespace seq {
             e->add_subst(s);
             child->apply_subst(m_sg, s);
             if (exp_n)
-                e->add_side_int(mk_int_constraint(exp_n, one, int_constraint_kind::ge, mem->m_dep));
+                e->add_side_constraint(mk_constraint(arith.mk_ge(exp_n, one), mem->m_dep));
         }
 
         return true;
@@ -3765,15 +3753,8 @@ namespace seq {
     // int_constraint display
     // -----------------------------------------------------------------------
 
-    std::ostream& int_constraint::display(std::ostream& out) const {
-        if (m_lhs) out << mk_pp(m_lhs, m_lhs.get_manager());
-        else out << "null";
-        switch (m_kind) {
-        case int_constraint_kind::eq: out << " = "; break;
-        case int_constraint_kind::le: out << " <= "; break;
-        case int_constraint_kind::ge: out << " >= "; break;
-        }
-        if (m_rhs) out << mk_pp(m_rhs, m_rhs.get_manager());
+    std::ostream& constraint::display(std::ostream& out) const {
+        if (fml) out << mk_pp(fml, fml.get_manager());
         else out << "null";
         return out;
     }
@@ -3783,21 +3764,6 @@ namespace seq {
     // Uses the injected simple_solver (default: lp_simple_solver).
     // -----------------------------------------------------------------------
 
-    expr_ref nielsen_graph::int_constraint_to_expr(int_constraint const& ic) {
-        ast_manager& m = m_sg.get_manager();
-        arith_util arith(m);
-        switch (ic.m_kind) {
-        case int_constraint_kind::eq:
-            return expr_ref(m.mk_eq(ic.m_lhs, ic.m_rhs), m);
-        case int_constraint_kind::le:
-            return expr_ref(arith.mk_le(ic.m_lhs, ic.m_rhs), m);
-        case int_constraint_kind::ge:
-            return expr_ref(arith.mk_ge(ic.m_lhs, ic.m_rhs), m);
-        }
-        UNREACHABLE();
-        return expr_ref(m.mk_true(), m);
-    }
-
     // -----------------------------------------------------------------------
     // Modification counter: substitution length tracking
     // mirrors ZIPT's LocalInfo.CurrentModificationCnt + NielsenEdge.IncModCount/DecModCount
@@ -3846,8 +3812,7 @@ namespace seq {
             expr_ref lhs = compute_length_expr(s.m_var);
             lhs_exprs.push_back({i, lhs.get()});
             // Assert LHS >= 0
-            e->add_side_int(int_constraint(lhs, arith.mk_int(0),
-                                           int_constraint_kind::ge, s.m_dep, m));
+            e->add_side_constraint(mk_constraint(arith.mk_ge(lhs, arith.mk_int(0)), s.m_dep));
         }
 
         // Step 2: Bump mod counts for all non-eliminating variables at once.
@@ -3865,8 +3830,7 @@ namespace seq {
             expr* lhs_expr = p.second;
             auto const& s = substs[idx];
             expr_ref rhs = compute_length_expr(s.m_replacement);
-            e->add_side_int(int_constraint(lhs_expr, rhs, int_constraint_kind::eq,
-                                           s.m_dep, m));
+            e->add_side_constraint(mk_constraint(m.mk_eq(lhs_expr, rhs), s.m_dep));
 
             // Assert non-negativity for any fresh length variables in the RHS
             // (variables at mod_count > 0 that are newly created).
@@ -3878,8 +3842,7 @@ namespace seq {
                     m_mod_cnt.find(tok->id(), mc);
                     if (mc > 0) {
                         expr_ref len_var = get_or_create_len_var(tok, mc);
-                        e->add_side_int(int_constraint(len_var, arith.mk_int(0),
-                                                       int_constraint_kind::ge, s.m_dep, m));
+                        e->add_side_constraint(mk_constraint(arith.mk_ge(len_var, arith.mk_int(0)), s.m_dep));
                     }
                 }
             }
@@ -3924,14 +3887,13 @@ namespace seq {
     }
 
     void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) {
-        // Assert only the int_constraints that are new to this node (beyond those
+        // Assert only the constraints that are new to this node (beyond those
         // inherited from its parent via clone_from).  The parent's constraints are
         // already present in the enclosing solver scope; asserting them again would
         // be redundant (though harmless).  This is called by search_dfs right after
         // simplify_and_init, which is where new constraints are produced.
-        for (unsigned i = node->m_parent_ic_count; i < node->int_constraints().size(); ++i) {
-            m_solver.assert_expr(int_constraint_to_expr(node->int_constraints()[i]));
-        }
+        for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i)
+            m_solver.assert_expr(node->constraints()[i].fml);
     }
 
     void nielsen_graph::generate_node_length_constraints(nielsen_node* node) {
@@ -3954,8 +3916,7 @@ namespace seq {
 
             expr_ref len_lhs = compute_length_expr(eq.m_lhs);
             expr_ref len_rhs = compute_length_expr(eq.m_rhs);
-            node->add_int_constraint(int_constraint(len_lhs, len_rhs,
-                                                     int_constraint_kind::eq, eq.m_dep, m));
+            node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep));
 
             // non-negativity for each variable (mod-count-aware)
             euf::snode_vector tokens;
@@ -3965,8 +3926,7 @@ namespace seq {
                 if (tok->is_var() && !seen_vars.contains(tok->id())) {
                     seen_vars.insert(tok->id());
                     expr_ref len_var = compute_length_expr(tok);
-                    node->add_int_constraint(int_constraint(len_var, arith.mk_int(0),
-                                                             int_constraint_kind::ge, eq.m_dep, m));
+                    node->add_constraint(mk_constraint(arith.mk_ge(len_var, arith.mk_int(0)), eq.m_dep));
                 }
             }
         }
@@ -3983,11 +3943,9 @@ namespace seq {
             expr_ref len_str = compute_length_expr(mem.m_str);
 
             if (min_len > 0)
-                node->add_int_constraint(int_constraint(len_str, arith.mk_int(min_len),
-                                                         int_constraint_kind::ge, mem.m_dep, m));
+                node->add_constraint(mk_constraint(arith.mk_ge(len_str, arith.mk_int(min_len)), mem.m_dep));
             if (max_len < UINT_MAX)
-                node->add_int_constraint(int_constraint(len_str, arith.mk_int(max_len),
-                                                         int_constraint_kind::le, mem.m_dep, m));
+                node->add_constraint(mk_constraint(arith.mk_le(len_str, arith.mk_int(max_len)), mem.m_dep));
 
             // non-negativity for string-side variables
             euf::snode_vector tokens;
@@ -3996,24 +3954,21 @@ namespace seq {
                 if (tok->is_var() && !seen_vars.contains(tok->id())) {
                     seen_vars.insert(tok->id());
                     expr_ref len_var = compute_length_expr(tok);
-                    node->add_int_constraint(int_constraint(len_var, arith.mk_int(0),
-                                                             int_constraint_kind::ge, mem.m_dep, m));
+                    node->add_constraint(mk_constraint(arith.mk_ge(len_var, arith.mk_int(0)), mem.m_dep));
                 }
             }
         }
     }
 
-    bool nielsen_graph::check_int_feasibility(nielsen_node* node, svector<nielsen_edge*> const& cur_path) {
+    bool nielsen_graph::check_int_feasibility(nielsen_node* node) {
         // In incremental mode the solver already holds all path constraints
-        // (root length constraints at the base level, edge side_int and node
-        // int_constraints pushed/popped as the DFS descends and backtracks).
+        // (root length constraints at the base level, edge side_constraints and node
+        // constraints pushed/popped as the DFS descends and backtracks).
         // A plain check() is therefore sufficient.
         return m_solver.check() != l_false;
     }
 
-    bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs,
-                                     nielsen_node* node,
-                                     svector<nielsen_edge*> const& cur_path) {
+    bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs, nielsen_node* node) {
         ast_manager& m = m_sg.get_manager();
         arith_util arith(m);
 
@@ -4030,10 +3985,21 @@ namespace seq {
         return result == l_false;
     }
 
-    int_constraint nielsen_graph::mk_int_constraint(expr* lhs, expr* rhs,
-                                                     int_constraint_kind kind,
-                                                     dep_tracker const& dep) {
-        return int_constraint(lhs, rhs, kind, dep, m_sg.get_manager());
+    constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep) {
+        return constraint(fml, dep, m_sg.get_manager());
+    }
+
+    vector<constraint> nielsen_graph::get_path_leaf_side_constraints() const {
+        vector<constraint> result;
+        for (nielsen_edge* e : m_cur_path)
+            for (constraint const& c : e->side_constraints())
+                result.push_back(c);
+        nielsen_node* leaf = m_cur_path.empty() ? m_root
+                           : m_cur_path.back()->tgt();
+        if (leaf)
+            for (constraint const& c : leaf->constraints())
+                result.push_back(c);
+        return result;
     }
 
     expr* nielsen_graph::get_power_exponent(euf::snode* power) {
@@ -4053,7 +4019,7 @@ namespace seq {
     bool nielsen_graph::solve_sat_path_raw(model_ref& mdl) {
         mdl = nullptr;
         if (m_sat_path.empty() && (!m_sat_node ||
-            (m_sat_node->int_constraints().empty() && m_sat_node->char_diseqs().empty() && m_sat_node->char_ranges().empty())))
+            (m_sat_node->constraints().empty() && m_sat_node->char_diseqs().empty() && m_sat_node->char_ranges().empty())))
             return false;
 
         // Re-assert the sat-path constraints into m_solver (which holds only root-level
@@ -4064,14 +4030,12 @@ namespace seq {
         IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";);
         m_solver.push();
         for (nielsen_edge* e : m_sat_path) {
-            for (auto const& ic : e->side_int()) {
-                m_solver.assert_expr(int_constraint_to_expr(ic));
-            }
+            for (auto const& ic : e->side_constraints())
+                m_solver.assert_expr(ic.fml);
         }
         if (m_sat_node) {
-            for (auto const& ic : m_sat_node->int_constraints()) {
-                m_solver.assert_expr(int_constraint_to_expr(ic));
-            }
+            for (auto const& ic : m_sat_node->constraints())
+                m_solver.assert_expr(ic.fml);
             for (auto const& dis : m_sat_node->char_diseqs()) {
                 vector<expr*> dist;
                 dist.reserve((unsigned)dis.m_value.size());
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 4aaccf0e1..1790d3109 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -454,25 +454,17 @@ namespace seq {
     // mirrors ZIPT's IntEq and IntLe
     // -----------------------------------------------
 
-    enum class int_constraint_kind {
-        eq,   // lhs = rhs
-        le,   // lhs <= rhs
-        ge,   // lhs >= rhs
-    };
-
     // integer constraint stored per nielsen_node, tracking arithmetic
     // relationships between length variables and power exponents.
     // mirrors ZIPT's IntEq / IntLe over Presburger arithmetic polynomials.
-    struct int_constraint {
-        expr_ref             m_lhs;    // left-hand side (arithmetic expression)
-        expr_ref             m_rhs;    // right-hand side (arithmetic expression)
-        int_constraint_kind  m_kind;   // eq, le, or ge
-        dep_tracker          m_dep;    // tracks which input constraints contributed
+    struct constraint {
+        expr_ref    fml;   // the formula (eq, le, or ge expression)
+        dep_tracker dep;   // tracks which input constraints contributed
 
-        int_constraint(ast_manager& m):
-            m_lhs(m), m_rhs(m), m_kind(int_constraint_kind::eq), m_dep(nullptr) {}
-        int_constraint(expr* lhs, expr* rhs, int_constraint_kind kind, dep_tracker const& dep, ast_manager& m):
-            m_lhs(lhs, m), m_rhs(rhs, m), m_kind(kind), m_dep(dep) {}
+        constraint(ast_manager& m):
+            fml(m), dep(nullptr) {}
+        constraint(expr* f, dep_tracker const& d, ast_manager& m):
+            fml(f, m), dep(d) {}
 
         std::ostream& display(std::ostream& out) const;
     };
@@ -484,7 +476,7 @@ namespace seq {
         nielsen_node*           m_tgt;
         vector<nielsen_subst>   m_subst;
         vector<char_subst>      m_char_subst;     // character-level substitutions (mirrors ZIPT's SubstC)
-        vector<int_constraint>  m_side_int;        // side constraints: integer equalities/inequalities
+        vector<constraint>      m_side_constraints;  // side constraints: integer equalities/inequalities
         bool                    m_is_progress;     // does this edge represent progress?
         bool                    m_len_constraints_computed = false; // lazily computed substitution length constraints
     public:
@@ -501,10 +493,8 @@ namespace seq {
         vector<char_subst> const& char_substs() const { return m_char_subst; }
         void add_char_subst(char_subst const& s) { m_char_subst.push_back(s); }
 
-
-        void add_side_int(int_constraint const& ic) { m_side_int.push_back(ic); }
-
-        vector<int_constraint> const& side_int() const { return m_side_int; }
+        void add_side_constraint(constraint const& ic) { m_side_constraints.push_back(ic); }
+        vector<constraint> const& side_constraints() const { return m_side_constraints; }
 
         bool is_progress() const { return m_is_progress; }
 
@@ -525,9 +515,9 @@ namespace seq {
         nielsen_graph&          m_graph;
 
         // constraints at this node
-        vector<str_eq>          m_str_eq;     // string equalities
-        vector<str_mem>         m_str_mem;    // regex memberships
-        vector<int_constraint>  m_int_constraints;  // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe)
+        vector<str_eq>     m_str_eq;        // string equalities
+        vector<str_mem>    m_str_mem;       // regex memberships
+        vector<constraint> m_constraints;   // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe)
 
         // per-variable integer bounds for len(var). Mirrors ZIPT's IntBounds.
         // key: snode id of the string variable.
@@ -558,8 +548,8 @@ namespace seq {
         // Parikh filter: set to true once apply_parikh_to_node has been applied
         // to this node. Prevents duplicate constraint generation across DFS runs.
         bool                    m_parikh_applied = false;
-        // number of int_constraints inherited from the parent node at clone time.
-        // int_constraints[0..m_parent_ic_count) are already asserted at the
+        // number of constraints inherited from the parent node at clone time.
+        // constraints[0..m_parent_ic_count) are already asserted at the
         // parent's solver scope; only [m_parent_ic_count..end) need to be
         // asserted when this node's solver scope is entered.
         unsigned                m_parent_ic_count = 0;
@@ -585,14 +575,14 @@ namespace seq {
 
         void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); }
         void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); }
-        void add_int_constraint(int_constraint const& ic) { m_int_constraints.push_back(ic); }
+        void add_constraint(constraint const& ic) { m_constraints.push_back(ic); }
 
-        vector<int_constraint> const& int_constraints() const { return m_int_constraints; }
-        vector<int_constraint>& int_constraints() { return m_int_constraints; }
+        vector<constraint> const& constraints() const { return m_constraints; }
+        vector<constraint>& constraints() { return m_constraints; }
 
         // IntBounds: tighten the lower bound for len(var).
         // Returns true if the bound was tightened (lb > current lower bound).
-        // When tightened without conflict, adds an int_constraint len(var) >= lb.
+        // When tightened without conflict, adds a constraint len(var) >= lb.
         // When lb > current upper bound, sets arithmetic conflict (no constraint added)
         // and still returns true (the bound value changed). Check is_general_conflict()
         // separately to distinguish tightening-with-conflict from normal tightening.
@@ -601,7 +591,7 @@ namespace seq {
 
         // IntBounds: tighten the upper bound for len(var).
         // Returns true if the bound was tightened (ub < current upper bound).
-        // When tightened without conflict, adds an int_constraint len(var) <= ub.
+        // When tightened without conflict, adds a constraint len(var) <= ub.
         // When current lower bound > ub, sets arithmetic conflict (no constraint added)
         // and still returns true (the bound value changed). Check is_general_conflict()
         // separately to distinguish tightening-with-conflict from normal tightening.
@@ -674,10 +664,9 @@ namespace seq {
         void apply_subst(euf::sgraph& sg, nielsen_subst const& s);
 
         // simplify all constraints at this node and initialize status.
-        // cur_path provides the path from root to this node so that the
-        // LP solver can be queried for deterministic power cancellation.
+        // Uses m_graph.m_cur_path for LP solver queries during deterministic power cancellation.
         // Returns proceed, conflict, satisfied, or restart.
-        simplify_result simplify_and_init(svector<nielsen_edge*> const& cur_path = svector<nielsen_edge*>());
+        simplify_result simplify_and_init();
 
         // true if all str_eqs are trivial and there are no str_mems
         bool is_satisfied() const;
@@ -759,6 +748,7 @@ namespace seq {
         nielsen_node*                 m_root = nullptr;
         nielsen_node*                 m_sat_node = nullptr;
         svector<nielsen_edge*>        m_sat_path;
+        svector<nielsen_edge*>        m_cur_path;   // path from root to the current DFS node
         unsigned                      m_run_idx = 0;
         unsigned                      m_depth_bound = 0;
         unsigned                      m_max_search_depth = 0;
@@ -863,6 +853,15 @@ namespace seq {
         // path of edges from root to sat_node (set when sat_node is set)
         svector<nielsen_edge*> const& sat_path() const { return m_sat_path; }
 
+        // current DFS path (valid during and after solve())
+        svector<nielsen_edge*> const& cur_path() const { return m_cur_path; }
+
+        // Collect all side constraints along the current path and at the leaf node.
+        // Returns the edge side_constraints for every edge on m_cur_path plus the
+        // constraints() of the leaf node (last edge's target, or root if path is empty).
+        // Intended for theory_nseq to extract assertions implied by the SAT leaf.
+        vector<constraint> get_path_leaf_side_constraints() const;
+
         // add constraints to the root node from external solver
         void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r);
         void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l);
@@ -961,7 +960,7 @@ namespace seq {
 
     private:
 
-        search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
+        search_result search_dfs(nielsen_node* node, unsigned depth);
 
         // Regex widening: overapproximate `str` by replacing variables with
         // the intersection of their primitive regex constraints (or Σ* if
@@ -981,7 +980,7 @@ namespace seq {
 
         // Apply the Parikh image filter to a node: generate modular length
         // constraints from regex memberships and append them to the node's
-        // int_constraints.  Also performs a lightweight feasibility pre-check;
+        // constraints.  Also performs a lightweight feasibility pre-check;
         // if a Parikh conflict is detected the node's conflict flag is set with
         // backtrack_reason::parikh_image.
         //
@@ -1113,14 +1112,14 @@ namespace seq {
         // Mirrors ZIPT's Constraint.Shared forwarding mechanism.
         void assert_root_constraints_to_solver();
 
-        // Assert the int_constraints of `node` that are new relative to its
+        // Assert the constraints of `node` that are new relative to its
         // parent (indices [m_parent_ic_count..end)) into the current solver scope.
         // Called by search_dfs after simplify_and_init so that the newly derived
         // bounds become visible to subsequent check() and check_lp_le() calls.
         void assert_node_new_int_constraints(nielsen_node* node);
 
         // Generate |LHS| = |RHS| length constraints for a non-root node's own
-        // string equalities and add them as int_constraints on the node.
+        // string equalities and add them as constraints on the node.
         // Called once per node (guarded by m_node_len_constraints_generated).
         // Uses compute_length_expr (mod-count-aware) so that variables with
         // non-zero modification counts get fresh length variables.
@@ -1133,16 +1132,16 @@ namespace seq {
         // m_solver by search_dfs via push/pop, so a plain check() suffices.
         // l_undef (resource limit / timeout) is treated as feasible so that the
         // search continues rather than reporting a false unsatisfiability.
-        bool check_int_feasibility(nielsen_node* node, svector<nielsen_edge*> const& cur_path);
+        bool check_int_feasibility(nielsen_node* node);
 
         // check whether lhs <= rhs is implied by the path constraints.
         // mirrors ZIPT's NielsenNode.IsLe(): temporarily asserts NOT(lhs <= rhs)
         // and returns true iff the result is unsatisfiable (i.e., lhs <= rhs is
         // entailed).  Path constraints are already in the solver incrementally.
-        bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* node, svector<nielsen_edge*> const& cur_path);
+        bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* node);
 
         // create an integer constraint: lhs <kind> rhs
-        int_constraint mk_int_constraint(expr* lhs, expr* rhs, int_constraint_kind kind, dep_tracker const& dep);
+        constraint mk_constraint(expr* fml, dep_tracker const& dep);
 
         // get the exponent expression from a power snode (arg(1))
         expr* get_power_exponent(euf::snode* power);
@@ -1150,9 +1149,6 @@ namespace seq {
         // create a fresh integer variable expression (for power exponents)
         expr_ref mk_fresh_int_var();
 
-        // convert an int_constraint to an expr* assertion
-        expr_ref int_constraint_to_expr(int_constraint const& ic);
-
         // -----------------------------------------------
         // Modification counter methods for substitution length tracking.
         // mirrors ZIPT's NielsenEdge.IncModCount / DecModCount and
diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp
index f9e7031fe..7d6373eb2 100644
--- a/src/smt/seq/seq_nielsen_pp.cpp
+++ b/src/smt/seq/seq_nielsen_pp.cpp
@@ -209,16 +209,10 @@ namespace seq {
         return dot_html_escape(os.str());
     }
 
-    // Helper: render an int_constraint as an HTML string for DOT edge labels.
-    static std::string int_constraint_html(int_constraint const& ic, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) {
-        std::string r = arith_expr_html(ic.m_lhs, names, next_id, m);
-        switch (ic.m_kind) {
-        case int_constraint_kind::eq: r += " = ";       break;
-        case int_constraint_kind::le: r += " &#8804; "; break; // ≤
-        case int_constraint_kind::ge: r += " &#8805; "; break; // ≥
-        }
-        r += arith_expr_html(ic.m_rhs, names, next_id, m);
-        return r;
+    // Helper: render a constraint as an HTML string for DOT edge labels.
+    static std::string constraint_html(constraint const& ic, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) {
+        if (ic.fml) return arith_expr_html(ic.fml, names, next_id, m);
+        return "null";
     }
 
     static std::string regex_expr_html(expr* e, ast_manager& m, seq_util& seq) {
@@ -499,9 +493,9 @@ namespace seq {
             }
         }
         // integer constraints
-        for (auto const& ic : m_int_constraints) {
+        for (auto const& ic : m_constraints) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
-            out << int_constraint_html(ic, names, next_id, m) << "<br/>";
+            out << constraint_html(ic, names, next_id, m) << "<br/>";
         }
 
         if (!any)
@@ -606,11 +600,11 @@ namespace seq {
                         << " &#8594; ?" << cs.m_val->id();
                 }
                 // side constraints: integer equalities/inequalities
-                for (auto const& ic : e->side_int()) {
+                for (auto const& ic : e->side_constraints()) {
                     if (!first) out << "<br/>";
                     first = false;
                     out << "<font color=\"gray\">"
-                        << int_constraint_html(ic, names, next_id, m)
+                        << constraint_html(ic, names, next_id, m)
                         << "</font>";
                 }
                 out << ">";
diff --git a/src/smt/seq/seq_parikh.cpp b/src/smt/seq/seq_parikh.cpp
index 199777864..0dfc60f0e 100644
--- a/src/smt/seq/seq_parikh.cpp
+++ b/src/smt/seq/seq_parikh.cpp
@@ -173,7 +173,7 @@ namespace seq {
     // -----------------------------------------------------------------------
 
     void seq_parikh::generate_parikh_constraints(str_mem const& mem,
-                                                  vector<int_constraint>& out) {
+                                                  vector<constraint>& out) {
         if (!mem.m_regex || !mem.m_str)
             return;
 
@@ -210,13 +210,11 @@ namespace seq {
         expr_ref stride_expr(a.mk_int(stride), m);
         expr_ref stride_k(a.mk_mul(stride_expr, k_var), m);
         expr_ref rhs(a.mk_add(min_expr, stride_k), m);
-        out.push_back(int_constraint(len_str, rhs,
-                                     int_constraint_kind::eq, mem.m_dep, m));
+        out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, m));
 
         // Constraint 2: k ≥ 0
         expr_ref zero(a.mk_int(0), m);
-        out.push_back(int_constraint(k_var, zero,
-                                     int_constraint_kind::ge, mem.m_dep, m));
+        out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, m));
 
         // Constraint 3 (optional): k ≤ max_k when max_len is bounded.
         // max_k = floor((max_len - min_len) / stride)
@@ -228,17 +226,16 @@ namespace seq {
             unsigned range = max_len - min_len;
             unsigned max_k = range / stride;
             expr_ref max_k_expr(a.mk_int(max_k), m);
-            out.push_back(int_constraint(k_var, max_k_expr,
-                                         int_constraint_kind::le, mem.m_dep, m));
+            out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, m));
         }
     }
 
     void seq_parikh::apply_to_node(nielsen_node& node) {
-        vector<int_constraint> constraints;
+        vector<constraint> constraints;
         for (str_mem const& mem : node.str_mems())
             generate_parikh_constraints(mem, constraints);
         for (auto& ic : constraints)
-            node.add_int_constraint(ic);
+            node.add_constraint(ic);
     }
 
     // -----------------------------------------------------------------------
diff --git a/src/smt/seq/seq_parikh.h b/src/smt/seq/seq_parikh.h
index 47ec26424..6afff8167 100644
--- a/src/smt/seq/seq_parikh.h
+++ b/src/smt/seq/seq_parikh.h
@@ -100,11 +100,11 @@ namespace seq {
         // Dependencies are copied from mem.m_dep.
         // Does nothing when min_len ≥ max_len (empty or fixed-length language).
         void generate_parikh_constraints(str_mem const& mem,
-                                         vector<int_constraint>& out);
+                                         vector<constraint>& out);
 
         // Apply Parikh constraints to all memberships at a node.
         // Calls generate_parikh_constraints for each str_mem in the node
-        // and appends the resulting int_constraints to node.int_constraints().
+        // and appends the resulting constraints to node.constraints().
         void apply_to_node(nielsen_node& node);
 
         // Quick Parikh feasibility check (no solver call).
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index f1d1f759f..b1c881328 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -3300,26 +3300,26 @@ static void test_add_lower_int_bound_basic() {
     // initially no bounds
     SASSERT(node->var_lb(x) == 0);
     SASSERT(node->var_ub(x) == UINT_MAX);
-    SASSERT(node->int_constraints().empty());
+    SASSERT(node->constraints().empty());
 
     // add lower bound lb=3: should tighten and add constraint
     bool tightened = node->add_lower_int_bound(x, 3, dep);
     SASSERT(tightened);
     SASSERT(node->var_lb(x) == 3);
-    SASSERT(node->int_constraints().size() == 1);
-    SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::ge);
+    SASSERT(node->constraints().size() == 1);
+    SASSERT(node->constraints()[0].fml);
 
     // add weaker lb=2: no tightening
     tightened = node->add_lower_int_bound(x, 2, dep);
     SASSERT(!tightened);
     SASSERT(node->var_lb(x) == 3);
-    SASSERT(node->int_constraints().size() == 1);
+    SASSERT(node->constraints().size() == 1);
 
     // add tighter lb=5: should tighten and add another constraint
     tightened = node->add_lower_int_bound(x, 5, dep);
     SASSERT(tightened);
     SASSERT(node->var_lb(x) == 5);
-    SASSERT(node->int_constraints().size() == 2);
+    SASSERT(node->constraints().size() == 2);
 
     std::cout << "  ok\n";
 }
@@ -3347,20 +3347,20 @@ static void test_add_upper_int_bound_basic() {
     bool tightened = node->add_upper_int_bound(x, 10, dep);
     SASSERT(tightened);
     SASSERT(node->var_ub(x) == 10);
-    SASSERT(node->int_constraints().size() == 1);
-    SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::le);
+    SASSERT(node->constraints().size() == 1);
+    SASSERT(node->constraints()[0].fml);
 
     // add weaker ub=20: no tightening
     tightened = node->add_upper_int_bound(x, 20, dep);
     SASSERT(!tightened);
     SASSERT(node->var_ub(x) == 10);
-    SASSERT(node->int_constraints().size() == 1);
+    SASSERT(node->constraints().size() == 1);
 
     // add tighter ub=5: tightens
     tightened = node->add_upper_int_bound(x, 5, dep);
     SASSERT(tightened);
     SASSERT(node->var_ub(x) == 5);
-    SASSERT(node->int_constraints().size() == 2);
+    SASSERT(node->constraints().size() == 2);
 
     std::cout << "  ok\n";
 }
@@ -3427,7 +3427,7 @@ static void test_bounds_cloned() {
     SASSERT(child->var_ub(y) == UINT_MAX);
 
     // child's int_constraints should also be cloned (3 constraints: lb_x, ub_x, lb_y)
-    SASSERT(child->int_constraints().size() == parent->int_constraints().size());
+    SASSERT(child->constraints().size() == parent->constraints().size());
 
     std::cout << "  ok\n";
 }
@@ -3454,7 +3454,7 @@ static void test_var_bound_watcher_single_var() {
     // set bounds: 3 <= len(x) <= 7
     node->add_lower_int_bound(x, 3, dep);
     node->add_upper_int_bound(x, 7, dep);
-    node->int_constraints().reset();  // clear for clean count
+    node->constraints().reset();  // clear for clean count
 
     // apply substitution x → a·y
     euf::snode* ay = sg.mk_concat(a, y);
@@ -3490,7 +3490,7 @@ static void test_var_bound_watcher_conflict() {
 
     // set bounds: 3 <= len(x)  (so x must have at least 3 chars)
     node->add_lower_int_bound(x, 3, dep);
-    node->int_constraints().reset();
+    node->constraints().reset();
 
     // apply substitution x → a·b (const_len=2 < lb=3)
     euf::snode* ab = sg.mk_concat(a, b);
@@ -3624,7 +3624,7 @@ static void test_var_bound_watcher_multi_var() {
 
     // set upper bound: len(x) <= 5
     node->add_upper_int_bound(x, 5, dep);
-    node->int_constraints().reset();
+    node->constraints().reset();
 
     // apply substitution x → y·z (two vars, no constants)
     euf::snode* yz = sg.mk_concat(y, z);
diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp
index 62af7535c..4d68feb0c 100644
--- a/src/test/seq_parikh.cpp
+++ b/src/test/seq_parikh.cpp
@@ -326,7 +326,7 @@ static void test_generate_constraints_ab_star() {
     seq::dep_tracker dep = dm.mk_leaf(lit);
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
-    vector<seq::int_constraint> out;
+    vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
 
     // expect at least: len(x)=0+2k and k>=0
@@ -337,19 +337,19 @@ static void test_generate_constraints_ab_star() {
     // check that one constraint is an equality (len(x) = 0 + 2·k)
     bool has_eq = false;
     for (auto const& ic : out)
-        if (ic.m_kind == seq::int_constraint_kind::eq) has_eq = true;
+        if (m.is_eq(ic.fml)) has_eq = true;
     SASSERT(has_eq);
 
     // check that one constraint is k >= 0
     bool has_ge = false;
     for (auto const& ic : out)
-        if (ic.m_kind == seq::int_constraint_kind::ge) has_ge = true;
+        if (arith.is_ge(ic.fml)) has_ge = true;
     SASSERT(has_ge);
 
     // should NOT have an upper bound (star is unbounded)
     bool has_le = false;
     for (auto const& ic : out)
-        if (ic.m_kind == seq::int_constraint_kind::le) has_le = true;
+        if (arith.is_le(ic.fml)) has_le = true;
     SASSERT(!has_le);
 }
 
@@ -361,6 +361,7 @@ static void test_generate_constraints_bounded_loop() {
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
     seq_util seq(m);
+    arith_util arith(m);
     seq::seq_parikh parikh(sg);
 
     euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@@ -372,7 +373,7 @@ static void test_generate_constraints_bounded_loop() {
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
-    vector<seq::int_constraint> out;
+    vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
 
     // expect: eq + ge + le = 3 constraints
@@ -381,9 +382,9 @@ static void test_generate_constraints_bounded_loop() {
 
     bool has_eq = false, has_ge = false, has_le = false;
     for (auto const& ic : out) {
-        if (ic.m_kind == seq::int_constraint_kind::eq)  has_eq = true;
-        if (ic.m_kind == seq::int_constraint_kind::ge)  has_ge = true;
-        if (ic.m_kind == seq::int_constraint_kind::le)  has_le = true;
+        if (m.is_eq(ic.fml))    has_eq = true;
+        if (arith.is_ge(ic.fml)) has_ge = true;
+        if (arith.is_le(ic.fml)) has_le = true;
     }
     SASSERT(has_eq);
     SASSERT(has_ge);
@@ -409,7 +410,7 @@ static void test_generate_constraints_stride_one() {
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
-    vector<seq::int_constraint> out;
+    vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
     std::cout << "  generated " << out.size() << " constraints (expect 0)\n";
     SASSERT(out.empty());
@@ -432,7 +433,7 @@ static void test_generate_constraints_fixed_length() {
     seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
-    vector<seq::int_constraint> out;
+    vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
     std::cout << "  generated " << out.size() << " constraints (expect 0)\n";
     SASSERT(out.empty());
@@ -456,14 +457,14 @@ static void test_generate_constraints_dep_propagated() {
     seq::dep_tracker dep = dm.mk_leaf(lit);
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
-    vector<seq::int_constraint> out;
+    vector<seq::constraint> out;
     parikh.generate_parikh_constraints(mem, out);
 
     // all generated constraints must carry dep_source{mem,7} in their dependency
     for (auto const& ic : out) {
-        SASSERT(ic.m_dep != nullptr);
+        SASSERT(ic.dep != nullptr);
         vector<seq::dep_source, false> vs;
-        dm.linearize(ic.m_dep, vs);
+        dm.linearize(ic.dep, vs);
         bool found = false;
         for (auto const& d : vs)
             if (std::get<sat::literal>(d) == lit) found = true;
@@ -495,11 +496,11 @@ static void test_apply_to_node_adds_constraints() {
 
     // root node should have no int_constraints initially
     SASSERT(ng.root() != nullptr);
-    unsigned before = ng.root()->int_constraints().size();
+    unsigned before = ng.root()->constraints().size();
 
     parikh.apply_to_node(*ng.root());
 
-    unsigned after = ng.root()->int_constraints().size();
+    unsigned after = ng.root()->constraints().size();
     std::cout << "  before=" << before << " after=" << after << "\n";
     SASSERT(after > before);
 }
@@ -525,9 +526,9 @@ static void test_apply_to_node_stride_one_no_constraints() {
     euf::snode* regex = sg.mk(re);
     ng.add_str_mem(x, regex);
 
-    unsigned before = ng.root()->int_constraints().size();
+    unsigned before = ng.root()->constraints().size();
     parikh.apply_to_node(*ng.root());
-    unsigned after = ng.root()->int_constraints().size();
+    unsigned after = ng.root()->constraints().size();
     std::cout << "  before=" << before << " after=" << after << " (expect no change)\n";
     SASSERT(after == before);
 }