Fix review: min>=max guard, ceiling-div overflow, SASSERT, accessor methods, comments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/smt/seq/nseq_parikh.cpp

@@ -211,9 +211,11 @@ namespace seq {
         unsigned min_len = seq.re.min_length(re_expr);
         unsigned max_len = seq.re.max_length(re_expr);
 
-        // If min_len == max_len the bounds already pin the length exactly;
-        // no modular constraint is needed.
-        if (min_len == max_len)
+        // If min_len >= max_len the bounds already pin the length exactly
+        // (or the language is empty — empty language is detected by simplify_and_init
+        // via Brzozowski derivative / is_empty checks, not here).
+        // We only generate modular constraints when the length is variable.
+        if (min_len >= max_len)
             return;
 
         unsigned stride = compute_length_stride(re_expr);
@@ -244,10 +246,12 @@ namespace seq {
 
         // Constraint 3 (optional): k ≤ max_k when max_len is bounded.
         // max_k = floor((max_len - min_len) / stride)
-        // This gives the solver an explicit upper bound on k, which tightens
-        // the search space when combined with other constraints on len(str).
+        // This gives the solver an explicit upper bound on k.
+        // The subtraction is safe because min_len < max_len is guaranteed
+        // by the early return above.
         if (max_len != UINT_MAX) {
-            unsigned range = max_len - min_len;  // max_len >= min_len here
+            SASSERT(max_len > min_len);
+            unsigned range = max_len - min_len;
             unsigned max_k = range / stride;
             expr_ref max_k_expr(arith.mk_int(max_k), m);
             out.push_back(int_constraint(k_var, max_k_expr,
@@ -291,6 +295,8 @@ namespace seq {
 
             unsigned stride = compute_length_stride(re_expr);
             if (stride <= 1) continue; // no useful modular constraint
+            // stride > 1 guaranteed from here onward.
+            SASSERT(stride > 1);
 
             unsigned lb = node.var_lb(mem.m_str);
             unsigned ub = node.var_ub(mem.m_str);
@@ -305,7 +311,14 @@ namespace seq {
             unsigned k_min = 0;
             if (lb > min_len) {
                 unsigned gap = lb - min_len;
-                k_min = (gap + stride - 1) / stride;  // ceiling division
+                // Ceiling division: k_min = ceil(gap / stride).
+                // Guard: (gap + stride - 1) may overflow if gap is close to UINT_MAX.
+                // In that case k_min would be huge, and min_len + stride*k_min would
+                // also overflow ub → treat as a conflict immediately.
+                if (gap > UINT_MAX - (stride - 1)) {
+                    return true; // ceiling division would overflow → k_min too large
+                }
+                k_min = (gap + stride - 1) / stride;
             }
 
             // Overflow guard: stride * k_min may overflow unsigned.

src/smt/seq/nseq_parith.h

@@ -88,12 +88,14 @@ namespace seq {
 
         // Generate Parikh modular length constraints for one membership.
         //
-        // When stride > 1 and min_len < max_len (bounds don't pin length):
+        // When stride > 1 and min_len < max_len (bounds don't pin length exactly,
+        // and the language is non-empty):
         //   adds: len(str) = min_len + stride · k   (equality)
         //         k ≥ 0                              (non-negativity)
         //         k ≤ (max_len - min_len) / stride   (upper bound, when max_len bounded)
         // These tighten the integer constraint set for the subsolver.
         // 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);
 

src/smt/seq/seq_nielsen.cpp

@@ -1047,8 +1047,8 @@ namespace seq {
         // contradict the variable's current integer bounds?  If so, mark this
         // node as a Parikh-image conflict immediately (avoids a solver call).
         if (!node.is_currently_conflict() && m_parith->check_parikh_conflict(node)) {
-            node.m_is_general_conflict = true;
-            node.m_reason = backtrack_reason::parikh_image;
+            node.set_general_conflict(true);
+            node.set_reason(backtrack_reason::parikh_image);
         }
     }
 
@@ -1152,6 +1152,8 @@ namespace seq {
         // Apply Parikh image filter: generate modular length constraints and
         // perform a lightweight feasibility pre-check.  The filter is guarded
         // internally (m_parikh_applied) so it only runs once per node.
+        // Note: Parikh filtering is skipped for satisfied nodes (returned above);
+        // a fully satisfied node has no remaining memberships to filter.
         apply_parikh_to_node(*node);
         if (node->is_currently_conflict()) {
             ++m_stats.m_num_simplify_conflict;