From dc8fcb93a60f999ba90eb6049c06873bff3c9945 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 04:59:52 +0000
Subject: [PATCH] Enable macro-finder fallback for auto_config=false mbqi=false

---
 src/params/smt_params.cpp |  7 ++++++-
 src/test/quant_solve.cpp  | 25 +++++++++++++++++++++++++
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp
index bd58aeb311..d1222a0a0c 100644
--- a/src/params/smt_params.cpp
+++ b/src/params/smt_params.cpp
@@ -71,6 +71,12 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_lemmas2console = sp.lemmas2console();
     m_instantiations2console = sp.instantiations2console();
     m_proof_log = sp.proof_log();
+
+    if (!m_auto_config && !m_mbqi &&
+        !_p.contains("macro_finder") && !_p.contains("smt.macro_finder") &&
+        !_p.contains("quasi_macros") && !_p.contains("smt.quasi_macros")) {
+        m_macro_finder = true;
+    }
     
 }
 
@@ -433,4 +439,3 @@ void smt_params::setup_LRA() {
     m_arith_propagate_eqs = false;
     m_eliminate_term_ite  = true;
 }
-
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 59e35d927e..357b58dc7b 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -198,6 +198,30 @@ static void test_qe_regression_4175() {
     }
 }
 
+static void test_macro_finder_fallback_8052() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    cmd_context ctx(false, &m);
+    ctx.set_ignore_check(true);
+    std::istringstream is(R"(
+(declare-fun f (Int) Int)
+(declare-const x Int)
+(assert (forall ((i Int)) (! (= (f i) i) :pattern ((f i)) :weight 0)))
+(assert (> x (f 0)))
+)");
+    VERIFY(parse_smt2_commands(ctx, is));
+
+    params_ref p;
+    p.set_bool("auto_config", false);
+    p.set_bool("mbqi", false);
+    p.set_uint("relevancy", 0);
+    smt_params params(p);
+    smt::kernel solver(m, params);
+    for (unsigned i = 0; i < ctx.assertions().size(); ++i)
+        solver.assert_expr(ctx.assertions().get(i));
+    VERIFY(l_true == solver.check());
+}
+
 
 static void test_quant_solve1() {
     ast_manager m;
@@ -284,6 +308,7 @@ void tst_quant_solve() {
 
     test_quant_solve1();   
     test_qe_regression_4175();
+    test_macro_finder_fallback_8052();
 
 #if 0
     memory::finalize();