Fix regression timeouts via range condition simplification

- Simplify trivial range bounds in derive_range: when lo=0, omit
  the lo<=x condition; when hi=max_char, omit the x<=hi condition.
  Full charset ranges return epsilon directly.

- Add char_le(0,x)=true and char_le(x,max)=true to eval_cond for
  always-valid bounds.

- Add range implication logic to simplify_ite_rec: when path has
  negated/positive char_le constraints, detect implied or contradicted
  char_le conditions (e.g., ¬(x<=127) implies 128<=x).

- Add is_subset(a, .+) check: non-nullable regexes are subsets of .+

- In update_state_graph, skip recursive exploration of nullable targets
  to avoid state explosion.

These fixes resolve timeouts on 5724 (all problems), 5721 P1, and 5693.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: NikolajBjorner

src/ast/rewriter/seq_derive.cpp

@@ -336,10 +336,22 @@ namespace seq {
         // Extract character values from unit strings
         expr_ref c_lo(m), c_hi(m);
         if (u().str.is_unit_string(lo, c_lo) && u().str.is_unit_string(hi, c_hi)) {
-            // ite(lo <= ele && ele <= hi, ε, ∅)
-            expr_ref ge_lo(m_util.mk_le(c_lo, m_ele), m);
-            expr_ref le_hi(m_util.mk_le(m_ele, c_hi), m);
-            expr_ref in_range(m.mk_and(ge_lo, le_hi), m);
+            // Build range condition, simplifying trivial bounds
+            unsigned lo_val = 0, hi_val = 0;
+            bool lo_trivial = m_util.is_const_char(c_lo, lo_val) && lo_val == 0;
+            bool hi_trivial = m_util.is_const_char(c_hi, hi_val) && hi_val == u().max_char();
+
+            if (lo_trivial && hi_trivial)
+                return eps; // full charset range — always matches
+
+            expr_ref in_range(m);
+            if (lo_trivial)
+                in_range = m_util.mk_le(m_ele, c_hi);
+            else if (hi_trivial)
+                in_range = m_util.mk_le(c_lo, m_ele);
+            else
+                in_range = m.mk_and(m_util.mk_le(c_lo, m_ele), m_util.mk_le(m_ele, c_hi));
+
             return mk_ite(in_range, eps, empty);
         }
 
@@ -508,8 +520,13 @@ namespace seq {
         if (re().is_empty(a)) return true;
         if (re().is_full_seq(b)) return true;
 
-        // a ⊆ a* (since a* accepts everything a does and more)
+        // a ⊆ .+ iff a is non-nullable (non-nullable means ε ∉ L(a))
         expr* b1 = nullptr;
+        if (re().is_plus(b, b1) && re().is_full_char(b1) &&
+            re().get_info(a).nullable == l_false)
+            return true;
+
+        // a ⊆ a* (since a* accepts everything a does and more)
         if (re().is_star(b, b1) && a == b1) return true;
 
         // a* ⊆ b* if a ⊆ b
@@ -964,6 +981,12 @@ namespace seq {
                 return vl <= vr ? l_true : l_false;
             if (u().is_const_char(lhs, vl) && u().is_const_char(rhs, vr))
                 return vl <= vr ? l_true : l_false;
+            // char_le(0, x) is always true (chars are unsigned)
+            if (u().is_const_char(lhs, vl) && vl == 0)
+                return l_true;
+            // char_le(x, max_char) is always true
+            if (u().is_const_char(rhs, vr) && vr == u().max_char())
+                return l_true;
         }
 
         // not(e1)
@@ -1074,6 +1097,52 @@ namespace seq {
                         return simplify_ite_rec(path, e);
                 }
             }
+
+            // Range implication between char_le conditions:
+            // If c is char_le(lo, x) [lo <= x] and path has ¬(x <= hi) [x > hi]:
+            //   ¬(x <= hi) means x >= hi+1. If lo <= hi+1, then lo <= x is implied → c is true.
+            // If c is char_le(x, hi) [x <= hi] and path has ¬(lo <= x) [x < lo]:
+            //   ¬(lo <= x) means x <= lo-1. If lo-1 <= hi, then x <= hi is implied → c is true.
+            expr* c_lhs = nullptr, * c_rhs = nullptr;
+            expr* p_lhs = nullptr, * p_rhs = nullptr;
+            if (m_util.is_char_le(c, c_lhs, c_rhs) && m_util.is_char_le(cond, p_lhs, p_rhs)) {
+                unsigned c_lo = 0, c_hi = 0, p_lo = 0, p_hi = 0;
+                if (sign) {
+                    // cond is negated (¬cond is true)
+                    // c is (lo <= x), cond is (x <= hi) with sign=true means ¬(x <= hi) i.e. x > hi i.e. x >= hi+1
+                    if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele &&
+                        p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) &&
+                        c_lo <= p_hi + 1)
+                        return simplify_ite_rec(path, t);
+                    // c is (x <= hi), cond is (lo <= x) with sign=true means ¬(lo <= x) i.e. x < lo i.e. x <= lo-1
+                    if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) &&
+                        m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele &&
+                        p_lo > 0 && p_lo - 1 <= c_hi)
+                        return simplify_ite_rec(path, t);
+                } else {
+                    // cond is true (not negated)
+                    // c is (lo <= x), cond is (x <= hi) true: x <= hi. If lo > hi → c is false.
+                    if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele &&
+                        p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) &&
+                        c_lo > p_hi)
+                        return simplify_ite_rec(path, e);
+                    // c is (x <= hi), cond is (lo <= x) true: lo <= x. If hi < lo → c is false.
+                    if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) &&
+                        m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele &&
+                        c_hi < p_lo)
+                        return simplify_ite_rec(path, e);
+                    // c is (lo <= x), cond is (lo2 <= x) true: lo2 <= x. If lo <= lo2 → c is true.
+                    if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele &&
+                        m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele &&
+                        c_lo <= p_lo)
+                        return simplify_ite_rec(path, t);
+                    // c is (x <= hi), cond is (x <= hi2) true: x <= hi2. If hi >= hi2 → c is true.
+                    if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) &&
+                        p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) &&
+                        c_hi >= p_hi)
+                        return simplify_ite_rec(path, t);
+                }
+            }
         }
 
         // Check if both range bounds are in path and c is (x = v) within range

src/smt/seq_regex.cpp

@@ -859,6 +859,16 @@ namespace smt {
                 m_state_graph.add_edge(r_id, dr_id, maybecycle);
             }
             m_state_graph.mark_done(r_id);
+            // Recursively explore unexplored targets for dead state detection
+            // Skip targets that are nullable to avoid state explosion
+            for (auto const& dr: derivatives) {
+                unsigned dr_id = get_state_id(dr);
+                if (m_state_graph.is_done(dr_id) || m_state_graph.is_live(dr_id))
+                    continue;
+                if (re().get_info(dr).nullable == l_true)
+                    continue;
+                update_state_graph(dr);
+            }
         }
 
         STRACE(seq_regex, m_state_graph.display(tout););