From 01633f7ce2ee273c23e4eb5cfe5f359deea74aa3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Jul 2025 16:22:08 -0700
Subject: [PATCH] respect smt configuration parameter in elim_unconstrained
 simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/elim_unconstrained.cpp | 17 ++++++++++++-----
 src/ast/simplifiers/elim_unconstrained.h   |  9 ++++++++-
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 48f8b9071..974b37a00 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -112,7 +112,7 @@ eliminate:
 --*/
 
 
-
+#include "params/smt_params_helper.hpp"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/recfun_decl_plugin.h"
@@ -166,7 +166,7 @@ void elim_unconstrained::eliminate() {
         expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
         bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r);
         proof_ref pr(m);
-        if (inverted && m_enable_proofs) {
+        if (inverted && m_config.m_enable_proofs) {
             expr * s    = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz);
             expr * eq   = m.mk_eq(s, r);
             proof * pr1 = m.mk_def_intro(eq);
@@ -267,7 +267,7 @@ void elim_unconstrained::reset_nodes() {
  */
 void elim_unconstrained::init_nodes() {
 
-    m_enable_proofs = false;
+    m_config.m_enable_proofs = false;
     m_trail.reset();
     m_fmls.freeze_suffix();
 
@@ -276,7 +276,7 @@ void elim_unconstrained::init_nodes() {
         auto [f, p, d] = m_fmls[i]();
         terms.push_back(f);
         if (p)
-            m_enable_proofs = true;
+            m_config.m_enable_proofs = true;
     }
 
     m_heap.reset();
@@ -303,7 +303,7 @@ void elim_unconstrained::init_nodes() {
     for (expr* e : terms)
         get_node(e).set_top();      
 
-    m_inverter.set_produce_proofs(m_enable_proofs);
+    m_inverter.set_produce_proofs(m_config.m_enable_proofs);
         
 }
 
@@ -422,6 +422,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
 }
 
 void elim_unconstrained::reduce() {
+    if (!m_config.m_enabled)
+        return;
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
@@ -436,3 +438,8 @@ void elim_unconstrained::reduce() {
         mc->reset();        
     }
 }
+
+void elim_unconstrained::updt_params(params_ref const& p) {
+    smt_params_helper sp(p);
+    m_config.m_enabled = sp.elim_unconstrained();
+}
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index 27f929453..4a248b44f 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -79,6 +79,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
         unsigned m_num_eliminated = 0;
         void reset() { m_num_eliminated = 0; }
     };
+    struct config {
+        bool m_enabled = true;
+        bool m_enable_proofs = false;
+    };
     expr_inverter            m_inverter;
     ptr_vector<node>         m_nodes;
     var_lt                   m_lt;
@@ -86,8 +90,8 @@ class elim_unconstrained : public dependent_expr_simplifier {
     expr_ref_vector          m_trail;
     expr_ref_vector          m_args;
     stats                    m_stats;
+    config                   m_config;
     bool                     m_created_compound = false;
-    bool                     m_enable_proofs = false;
 
     bool is_var_lt(int v1, int v2) const;
     node& get_node(unsigned n) const { return *m_nodes[n]; }
@@ -119,4 +123,7 @@ public:
     void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }
 
     void reset_statistics() override { m_stats.reset(); }
+
+    void updt_params(params_ref const& p) override;
+    
 };