From 0ca1668cce16888de2e1e2efdebbec12a935a329 Mon Sep 17 00:00:00 2001
From: GitHub Actions Bot <actions@github.com>
Date: Sat, 31 Jan 2026 23:28:57 +0000
Subject: [PATCH] Fix unused parameter warnings in empty function
 implementations

Remove unused parameter names from empty function bodies to eliminate
compiler warnings about unused parameters. This is a purely syntactic
change that does not affect program behavior.

Changes:
- Removed parameter names from empty updt_params() functions
- Removed parameter names from empty callback functions (merge_eh, etc.)
- Removed parameter names from empty interface implementations
- Affected 16 files across rewriters, solvers, and test code

These changes eliminate -Wunused-parameter warnings without changing
any functionality or breaking existing code.
---
 src/ast/rewriter/arith_rewriter.h      | 2 +-
 src/ast/rewriter/enum2bv_rewriter.cpp  | 2 +-
 src/ast/rewriter/pb_rewriter.h         | 4 ++--
 src/ast/sls/sls_smt_plugin.h           | 2 +-
 src/ast/sls/sls_smt_solver.h           | 2 +-
 src/math/lp/emonics.h                  | 4 ++--
 src/smt/seq_regex.h                    | 2 +-
 src/smt/smt_kernel.h                   | 6 +++---
 src/smt/theory_seq.h                   | 6 +++---
 src/smt/theory_special_relations.h     | 2 +-
 src/smt/theory_utvpi.h                 | 2 +-
 src/tactic/arith/nla2bv_tactic.cpp     | 2 +-
 src/tactic/bv/bvarray2uf_rewriter.h    | 2 +-
 src/tactic/core/injectivity_tactic.cpp | 2 +-
 src/test/im_float_config.h             | 4 ++--
 src/test/var_subst.cpp                 | 4 ++--
 16 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 9c1a0aba9..d38a859f6 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -40,7 +40,7 @@ protected:
     bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
     bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); }
-    void normalize(numeral & c, sort * s) {}
+    void normalize(numeral &, sort *) {}
     app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); }
     decl_kind add_decl_kind() const { return OP_ADD; }
     decl_kind mul_decl_kind() const { return OP_MUL; }
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index a8171c230..1054e60f3 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -272,7 +272,7 @@ struct enum2bv_rewriter::imp {
         m_rw(*this, m, p) {
     }
 
-    void updt_params(params_ref const & p) {}
+    void updt_params(params_ref const &) {}
     unsigned get_num_steps() const { return m_rw.get_num_steps(); }
     void cleanup() { m_rw.cleanup(); }
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
diff --git a/src/ast/rewriter/pb_rewriter.h b/src/ast/rewriter/pb_rewriter.h
index 8057c847b..29b4d26cc 100644
--- a/src/ast/rewriter/pb_rewriter.h
+++ b/src/ast/rewriter/pb_rewriter.h
@@ -51,8 +51,8 @@ public:
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
 
-    void updt_params(params_ref const & p) {}
-    static void get_param_descrs(param_descrs & r) {}
+    void updt_params(params_ref const &) {}
+    static void get_param_descrs(param_descrs &) {}
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
 
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index d3a1077ea..5316372c3 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -113,7 +113,7 @@ namespace sls {
         void check(expr_ref_vector const& fmls, vector <sat::literal_vector> const& clauses);
         void finalize(model_ref& md, ::statistics& st);
         void get_shared_clauses(vector<sat::literal_vector>& clauses);
-        void updt_params(params_ref& p) {}
+        void updt_params(params_ref&) {}
         std::ostream& display(std::ostream& out) override;
 
         void bounded_run(unsigned max_iterations);
diff --git a/src/ast/sls/sls_smt_solver.h b/src/ast/sls/sls_smt_solver.h
index 6f24b708d..566382d3a 100644
--- a/src/ast/sls/sls_smt_solver.h
+++ b/src/ast/sls/sls_smt_solver.h
@@ -36,7 +36,7 @@ namespace sls {
         void assert_expr(expr* e);
         lbool check();
         model_ref get_model();
-        void updt_params(params_ref& p) {}
+        void updt_params(params_ref&) {}
         void collect_statistics(statistics& st);
         std::ostream& display(std::ostream& out);
         void reset_statistics();
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 52b07cbb3..8ca9493ee 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -138,8 +138,8 @@ public:
         TRACE(nla_solver, tout << "unmerged " << i << " and " << j << "\n";);
     }
     
-    void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
-    void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
+    void merge_eh(unsigned, unsigned, unsigned, unsigned) {}
+    void after_merge_eh(unsigned, unsigned, unsigned, unsigned) {}
 
     void set_propagated(monic const& m);
     void set_bound_propagated(monic const& m);
diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h
index 5c3fddd25..6eeceda6f 100644
--- a/src/smt/seq_regex.h
+++ b/src/smt/seq_regex.h
@@ -189,7 +189,7 @@ namespace smt {
         seq_regex(theory_seq& th);
 
         void push_scope() {}
-        void pop_scope(unsigned num_scopes) {}
+        void pop_scope(unsigned) {}
         bool can_propagate() const { return false; }
         bool propagate() const { return false; }
 
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index 98b677213..fa517d5b4 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -154,10 +154,10 @@ namespace smt {
            \brief control phase selection and variable ordering.
            Base implementation is a no-op.
         */
-        void set_phase(expr * e) { }
+        void set_phase(expr *) { }
         solver::phase* get_phase() { return nullptr; }
-        void set_phase(solver::phase* p) { }
-        void move_to_front(expr* e) { }
+        void set_phase(solver::phase*) { }
+        void move_to_front(expr*) { }
 
         /**
            \brief Return the model associated with the last check command.
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 800fe5600..9ab40a35a 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -632,9 +632,9 @@ namespace smt {
         app* mk_value(app* a);
 
         trail_stack& get_trail_stack() { return m_trail_stack; }
-        void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
-        void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
-        void unmerge_eh(theory_var v1, theory_var v2) {}
+        void merge_eh(theory_var, theory_var, theory_var, theory_var) {}
+        void after_merge_eh(theory_var, theory_var, theory_var, theory_var) { }
+        void unmerge_eh(theory_var, theory_var) {}
 
         // eq_solver callbacks
         void add_consequence(bool uses_eq, expr_ref_vector const& clause) override;
diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h
index 085ecfe74..b0d2d0622 100644
--- a/src/smt/theory_special_relations.h
+++ b/src/smt/theory_special_relations.h
@@ -118,7 +118,7 @@ namespace smt {
             void operator()(literal_vector const & ex) {
                 m_explanation.append(ex);
             }
-            void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {}
+            void new_edge(dl_var, dl_var, unsigned, edge_id const*) {}
 
             bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j);
             bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j);
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index a917910e9..a58ca38b4 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -181,7 +181,7 @@ namespace smt {
         // Set a conflict due to a negative cycle.
         void set_conflict();
                
-        void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {}
+        void new_edge(dl_var, dl_var, unsigned, edge_id const*) {}
 
         // Create a new theory variable.
         th_var mk_var(enode* n) override;
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index f44ee1b84..d3eba22a5 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -79,7 +79,7 @@ class nla2bv_tactic : public tactic {
             m_default_bv_size = m_num_bits = p.get_uint("nla2bv_bv_size", 4);
         }
 
-        void updt_params(params_ref const& p)  {} 
+        void updt_params(params_ref const&)  {} 
         
         void operator()(goal & g, model_converter_ref & mc) {
             TRACE(nla2bv, g.display(tout);
diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h
index d6733d4a6..5b6403835 100644
--- a/src/tactic/bv/bvarray2uf_rewriter.h
+++ b/src/tactic/bv/bvarray2uf_rewriter.h
@@ -37,7 +37,7 @@ public:
     ~bvarray2uf_rewriter_cfg();
 
     ast_manager & m() const { return m_manager; }
-    void updt_params(params_ref const & p) {}
+    void updt_params(params_ref const &) {}
 
     void reset();
 
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index eb6470ace..cb210aee5 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -150,7 +150,7 @@ class injectivity_tactic : public tactic {
             }
         }
 
-        void updt_params(params_ref const & p) {}
+        void updt_params(params_ref const &) {}
     };
 
     struct rewriter_eq_cfg : public default_rewriter_cfg {
diff --git a/src/test/im_float_config.h b/src/test/im_float_config.h
index 3aab65836..9d8a05e2b 100644
--- a/src/test/im_float_config.h
+++ b/src/test/im_float_config.h
@@ -53,8 +53,8 @@ public:
     // Setters
     void set_lower(interval & a, numeral const & n) { m_manager.set(a.m_lower, n); }
     void set_upper(interval & a, numeral const & n) { m_manager.set(a.m_upper, n); }
-    void set_lower_is_open(interval & a, bool v) {}
-    void set_upper_is_open(interval & a, bool v) {}
+    void set_lower_is_open(interval &, bool) {}
+    void set_upper_is_open(interval &, bool) {}
     void set_lower_is_inf(interval & a, bool v) { if (v) m_manager.m().mk_ninf(m_manager.ebits(), m_manager.sbits(), a.m_lower); }
     void set_upper_is_inf(interval & a, bool v) { if (v) m_manager.m().mk_pinf(m_manager.ebits(), m_manager.sbits(), a.m_upper); }
     
diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp
index 36d5e8f03..1c5d58abe 100644
--- a/src/test/var_subst.cpp
+++ b/src/test/var_subst.cpp
@@ -29,8 +29,8 @@ namespace find_q {
     struct proc {
         quantifier * m_q;
         proc():m_q(nullptr) {}
-        void operator()(var * n) {}
-        void operator()(app * n) {}
+        void operator()(var *) {}
+        void operator()(app *) {}
         void operator()(quantifier * n) { m_q = n; }
     };
 };