From 6af8b4a11d2f89f37a78f12c5b011dd41429f043 Mon Sep 17 00:00:00 2001
From: Margus Veanes <margus@microsoft.com>
Date: Fri, 26 Jun 2026 08:47:55 +0300
Subject: [PATCH] Detect empty regex membership via re_is_empty fallback; fix
 test build

block_if_empty relied solely on the AST-identity state graph for dead-state
detection, which never closes on intersections/complements whose derivative
product states do not canonicalize. For ground regexes, fall back to the
antimirov NFA reachability check (re_is_empty), the same procedure propagate_eq
already uses for re.none equalities. Resolves str.in_re emptiness timeouts on
inter(., comp(.)) regexes (e.g. z3test 5728, parts of 5721).

Also drop a stale is_antimirov_union reference left in seq_regex_bisim.cpp after
the operator removal (test-z3 did not compile) and update a now-stale comment.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/seq_rewriter.h |  2 +-
 src/smt/seq_regex.cpp           | 11 +++++++++++
 src/test/seq_regex_bisim.cpp    |  2 +-
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 45821c8042..695e9ad876 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -445,7 +445,7 @@ public:
     variable v0 = (:var 0). Unlike `mk_derivative` this entry point keeps
     the symbolic derivative as a single transition regex (TRegex): boolean
     operators are pushed into the ITE leaves rather than lifted to the top
-    via _OP_RE_ANTIMIROV_UNION. Used by the regex_bisim equivalence
+    as a union. Used by the regex_bisim equivalence
     procedure which relies on each leaf of D(p XOR q) being a coherent
     XOR pair (D_v p) XOR (D_v q).
     */
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 45c70097c1..08852a2a12 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -224,6 +224,17 @@ namespace smt {
                 th.add_axiom(~lit);
                 return true;
             }
+            // Fall back to antimirov NFA reachability.  The lazy state graph
+            // keys states by AST identity and cannot close on intersections /
+            // complements whose derivative product states do not canonicalize,
+            // so it never detects their emptiness.  re_is_empty decides
+            // emptiness directly (the same procedure propagate_eq already uses
+            // for re.none equalities).
+            if (re_is_empty(r) == l_true) {
+                STRACE(seq_regex_brief, tout << "(empty:re) ";);
+                th.add_axiom(~lit);
+                return true;
+            }
         }
         return false;
     }
diff --git a/src/test/seq_regex_bisim.cpp b/src/test/seq_regex_bisim.cpp
index 83404439b5..49a96e8c20 100644
--- a/src/test/seq_regex_bisim.cpp
+++ b/src/test/seq_regex_bisim.cpp
@@ -49,7 +49,7 @@ static void test_a_star_neq_ab_star() {
     expr_ref_vector leaves(m);
     auto collect = [&](expr* e, auto&& self) -> void {
         expr* c, *t, *f;
-        if (m.is_ite(e, c, t, f) || u.re.is_union(e, t, f) || u.re.is_antimirov_union(e, t, f)) {
+        if (m.is_ite(e, c, t, f) || u.re.is_union(e, t, f)) {
             self(t, self);
             self(f, self);
             return;