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

@@ -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; }

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

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

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

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();

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

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; }
 

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.

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;

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

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;

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

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();
 

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 {

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); }
     

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; }
     };
 };