From af33dfaa7d699686972c9649d5b4c07602fb1768 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 21 May 2026 10:37:15 -0700
Subject: [PATCH] detect quantifiers in patterns

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/pattern/pattern_inference.cpp | 21 +++++++++++++++++++++
 src/ast/rewriter/rewriter_def.h       |  6 +++++-
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 6d3518de0..32b0546e8 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -254,6 +254,27 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
         }
         return;
     }
+    case AST_QUANTIFIER: {
+        quantifier * q = to_quantifier(n);
+        unsigned num_decls = q->get_num_decls();
+        info * body_info = nullptr;
+        m_cache.find(entry(q->get_expr(), delta + num_decls), body_info);
+        if (body_info == nullptr) {
+            save(n, delta, nullptr);
+            return;
+        }
+        // The lambda/quantifier itself is a valid sub-term in a pattern.
+        // Propagate the free variables from the body (they already refer
+        // to the outer quantifier's bindings) and keep the node as-is.
+        expr * new_body = body_info->m_node.get();
+        quantifier_ref new_q(m);
+        if (new_body != q->get_expr())
+            new_q = m.update_quantifier(q, new_body);
+        else
+            new_q = q;
+        save(n, delta, alloc(info, m, new_q, body_info->m_free_vars, body_info->m_size + 1));
+        return;
+    }
     default:
         save(n, delta, nullptr);
         return;
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index ebfc71482..7a395006d 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -561,9 +561,13 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
         expr * const * np  = it + 1;
         expr * const * nnp = np + num_pats;
         unsigned j = 0;
-        for (unsigned i = 0; i < num_pats; ++i)
+        for (unsigned i = 0; i < num_pats; ++i) {
             if (m_manager.is_pattern(np[i]))
                 new_pats[j++] = np[i];
+            else {
+                IF_VERBOSE(10, verbose_stream() << "[rewriter] dropping pattern (is_pattern check failed) for qid=" << q->get_qid() << " pattern[" << i << "]: " << mk_ismt2_pp(np[i], m_manager, 3) << "\n";);
+            }
+        }
         new_pats.shrink(j);
         num_pats = j;
         j = 0;