From 3d2d793f1d8f6449cd9c0f62dd7a3d67a460e160 Mon Sep 17 00:00:00 2001
From: Margus Veanes <margus@microsoft.com>
Date: Mon, 15 Jun 2026 03:18:15 -0700
Subject: [PATCH] fix(seq::derive): remove unsound depth limit in hoist_ite

The single-ITE branch of hoist_ite was gated by 'm_path_stack.size() < 8'.
When the depth limit was reached, hoist_ite returned nullptr and callers
fell back to non-path-aware structural rewrites (mk_union0 / mk_xor0).
These rewrites simplify e.g. mk_union(empty, X) -> X and return X unchanged,
preserving inner ITE branches that were built at an earlier (less constrained)
path. Subsequent derivative computation never path-prunes those branches,
which can leak unreachable epsilon-leaves into the final t-regex and cause
the bisimulation algorithm to report inequivalence for equivalent regexes.

Concrete trigger: derivatives of unions/xors with >= 9 components produce
9-deep ITE chains; at depth 8 the inner ITE returns unprocessed, leaving an
unreachable epsilon-leaf that bisim mis-interprets as a distinguishing word.

Removing the guard restores soundness. The corpus run against
regex-equivalence (1523 files) fixes 22 triangulated soundness bugs
(mut_0013, mut_0241, mut_0257, mut_0301 among others) with zero regressions.
89/89 unit tests pass.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/seq_derive.cpp | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 7c6ddf991..d98885235 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -1021,7 +1021,7 @@ namespace seq {
     }
 
     // Common ITE dispatch for binary ops (union/inter).
-    // Returns nullptr if neither a nor b is ITE (or depth limit reached).
+    // Returns nullptr if neither a nor b is ITE.
     expr_ref derive::hoist_ite(expr* a, expr* b, std::function<expr_ref(expr*, expr*)> apply_op) {
         expr *c1, *t1, *e1, *c2, *t2, *e2;
         if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2) && c1->get_id() > c2->get_id()) 
@@ -1035,17 +1035,18 @@ namespace seq {
             if (r) return r;
             return expr_ref(re().mk_empty(a->get_sort()), m);
         }
-        if (m_path_stack.size() < 8) {
-            if (m.is_ite(a, c1, t1, e1)) {
-                expr_ref r = apply_ite(c1, t1, e1, b, apply_op);
-                if (r) return r;
-                return expr_ref(re().mk_empty(a->get_sort()), m);
-            }
-            if (m.is_ite(b, c2, t2, e2)) {
-                expr_ref r = apply_ite(c2, t2, e2, a, apply_op);
-                if (r) return r;
-                return expr_ref(re().mk_empty(a->get_sort()), m);
-            }
+        // Single-ITE hoisting: must always recurse to maintain path-aware
+        // soundness — falling back to a non-path-aware structural rewrite
+        // here would bake unreachable branches into the result tree.
+        if (m.is_ite(a, c1, t1, e1)) {
+            expr_ref r = apply_ite(c1, t1, e1, b, apply_op);
+            if (r) return r;
+            return expr_ref(re().mk_empty(a->get_sort()), m);
+        }
+        if (m.is_ite(b, c2, t2, e2)) {
+            expr_ref r = apply_ite(c2, t2, e2, a, apply_op);
+            if (r) return r;
+            return expr_ref(re().mk_empty(a->get_sort()), m);
         }
         return expr_ref(nullptr, m);
     }