From 7040a74d1a55b3472ab10930d89aa350f039d06e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Jul 2026 14:59:50 -0700
Subject: [PATCH] defer ho-matching to lazy mam

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_quantifier.cpp | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 156f9ef80a..68358e3b02 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -867,10 +867,7 @@ namespace smt {
                                << " compiled=" << (p1 != mp) 
                                << " p1=" << mk_pp(p1, m) << "\n");
                     if (p1 != mp) {
-                        if (!unary && j >= num_eager_multi_patterns)
-                            m_lazy_mam->add_pattern(q1, p1);
-                        else
-                            m_mam->add_pattern(q1, p1);
+                        m_lazy_mam->add_pattern(q1, p1);
                     }
                 }
                 if (!unary)