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;