ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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) {

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;