From a6c51df1447e0499eee5f2a10d1224863b4015ec Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Jul 2025 14:54:15 -0700
Subject: [PATCH] ensure solve_eqs is fully disabled when smt.solve_eqs=false,
 #7743

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/solve_eqs.cpp | 6 ++++++
 src/ast/simplifiers/solve_eqs.h   | 1 +
 2 files changed, 7 insertions(+)

diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 8e293cbfe..71484590a 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -46,6 +46,7 @@ Outline of a presumably better scheme:
 #include "ast/simplifiers/solve_context_eqs.h"
 #include "ast/converters/generic_model_converter.h"
 #include "params/tactic_params.hpp"
+#include "params/smt_params_helper.hpp"
 
 
 namespace euf {
@@ -224,6 +225,9 @@ namespace euf {
     
     void solve_eqs::reduce() {
 
+        if (!m_config.m_enabled)
+            return;
+
         m_fmls.freeze_suffix();
 
         for (extract_eq* ex : m_extract_plugins)
@@ -330,6 +334,8 @@ namespace euf {
         for (auto* ex : m_extract_plugins)
             ex->updt_params(p);
         m_rewriter.updt_params(p);
+        smt_params_helper sp(p);
+        m_config.m_enabled = sp.solve_eqs();
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {
diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h
index dde42dd94..4e3ae6aa1 100644
--- a/src/ast/simplifiers/solve_eqs.h
+++ b/src/ast/simplifiers/solve_eqs.h
@@ -41,6 +41,7 @@ namespace euf {
         struct config {
             bool m_context_solve = true;
             unsigned m_max_occs = UINT_MAX;
+            bool m_enabled = true;
         };
 
         stats                         m_stats;