diff --git a/src/ast/rewriter/seq_regex_live.cpp b/src/ast/rewriter/seq_regex_live.cpp
index bd2196e438..d5fdcd5bf2 100644
--- a/src/ast/rewriter/seq_regex_live.cpp
+++ b/src/ast/rewriter/seq_regex_live.cpp
@@ -24,7 +24,6 @@ namespace seq {
         uint_set m_seen;
         vector<svector<unsigned>> m_predecessors;
         bool_vector m_live;
-        bool_vector m_closed;
         svector<unsigned> m_live_frontier;
         unsigned m_root_id = 0;
         failure m_failure = failure::none;
@@ -76,8 +75,6 @@ namespace seq {
                 s.m_predecessors.resize(size);
             if (s.m_live.size() < size)
                 s.m_live.resize(size, false);
-            if (s.m_closed.size() < size)
-                s.m_closed.resize(size, false);
         }
 
         char nullable(unsigned id) {
@@ -143,10 +140,22 @@ namespace seq {
             return true;
         }
 
+        /*
+          Reaching this point means the queue drained without hitting the state cap or a
+          resource limit, so m_to_explore is the complete, fully expanded forward cone of
+          the root and any state in it that liveness never reached has empty language --
+          a verdict that holds for every root, not just this one.
+
+          That verdict used to be recorded per search in a m_closed bit vector which no
+          caller ever read.  Retaining it globally and pruning on it was measured and does
+          not pay: by the time close() can prove a state empty, the search has already
+          expanded it and its whole cone, so the only work saved is on revisits, which the
+          successor, cofactor and product-visited caches already make cheap.  Over the
+          bench regexes corpus the result was -1.3% (seq monadic path) and +1.2% (legacy
+          path), and +1.7% on a QF_S sample, with no benchmark decided either way.  A
+          filter has to prune before exploration to be worth its lookups.
+        */
         void close(search& s) {
-            for (unsigned id : s.m_to_explore)
-                if (!s.m_live[id])
-                    s.m_closed[id] = true;
             s.m_complete = true;
         }