From c5b28950d519316494462a6c6f0e25fa0ad9be1b Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 14 Jan 2026 18:41:26 +0000
Subject: [PATCH] Remove redundant overridden default destructors (#8191)

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/simplifiers/bv_bounds_simplifier.cpp | 2 --
 src/ast/simplifiers/euf_completion.h         | 1 -
 src/ast/sls/sls_arith_base.h                 | 1 -
 src/ast/sls/sls_arith_plugin.h               | 1 -
 src/ast/sls/sls_array_plugin.h               | 1 -
 src/ast/sls/sls_basic_plugin.h               | 1 -
 src/ast/sls/sls_bv_plugin.h                  | 1 -
 src/ast/sls/sls_datatype_plugin.h            | 1 -
 src/ast/sls/sls_euf_plugin.h                 | 1 -
 src/ast/sls/sls_seq_plugin.h                 | 1 -
 src/qe/mbp/mbp_euf.h                         | 1 -
 src/sat/sat_ddfw_wrapper.h                   | 2 --
 src/smt/theory_intblast.h                    | 1 -
 src/smt/theory_sls.h                         | 1 -
 14 files changed, 16 deletions(-)

diff --git a/src/ast/simplifiers/bv_bounds_simplifier.cpp b/src/ast/simplifiers/bv_bounds_simplifier.cpp
index e1f4f2817..6bea2c3bb 100644
--- a/src/ast/simplifiers/bv_bounds_simplifier.cpp
+++ b/src/ast/simplifiers/bv_bounds_simplifier.cpp
@@ -25,8 +25,6 @@ public:
         updt_params(p);
     }
     
-    ~dom_bv_bounds_simplifier() override = default;
-    
     void updt_params(params_ref const & p) override {
         m_propagate_eq = p.get_bool("propagate_eq", false);
     }
diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h
index 2e8424a2a..97fc45a42 100644
--- a/src/ast/simplifiers/euf_completion.h
+++ b/src/ast/simplifiers/euf_completion.h
@@ -226,7 +226,6 @@ namespace euf {
         bool is_gt(expr* a, expr* b) const;
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
-        ~completion() override = default;
         char const* name() const override { return "euf-completion"; }
         void push() override;
         void pop(unsigned n) override;
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index 18d496dff..e42195001 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -348,7 +348,6 @@ namespace sls {
         bool update_num(var_t v, num_t const& delta);
     public:
         arith_base(context& ctx);
-        ~arith_base() override = default;
         void register_term(expr* e) override;
         bool set_value(expr* e, expr* v) override;
         expr_ref get_value(expr* e) override;
diff --git a/src/ast/sls/sls_arith_plugin.h b/src/ast/sls/sls_arith_plugin.h
index 6b18714e3..9ec959025 100644
--- a/src/ast/sls/sls_arith_plugin.h
+++ b/src/ast/sls/sls_arith_plugin.h
@@ -29,7 +29,6 @@ namespace sls {
         void init_backup();
     public:
         arith_plugin(context& ctx);
-        ~arith_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h
index 9726672dd..4040e8d57 100644
--- a/src/ast/sls/sls_array_plugin.h
+++ b/src/ast/sls/sls_array_plugin.h
@@ -115,7 +115,6 @@ namespace sls {
         
     public:
         array_plugin(context& ctx);
-        ~array_plugin() override = default;
         void register_term(expr* e) override { if (a.is_array(e->get_sort())) m_has_arrays = true; }
         expr_ref get_value(expr* e) override;
         void initialize() override { m_g = nullptr; }
diff --git a/src/ast/sls/sls_basic_plugin.h b/src/ast/sls/sls_basic_plugin.h
index 600ec3b30..c6d8d89b5 100644
--- a/src/ast/sls/sls_basic_plugin.h
+++ b/src/ast/sls/sls_basic_plugin.h
@@ -36,7 +36,6 @@ namespace sls {
             plugin(ctx) { 
             m_fid = basic_family_id;
         }
-        ~basic_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void initialize() override;
diff --git a/src/ast/sls/sls_bv_plugin.h b/src/ast/sls/sls_bv_plugin.h
index fd983a8fd..6d769f0f5 100644
--- a/src/ast/sls/sls_bv_plugin.h
+++ b/src/ast/sls/sls_bv_plugin.h
@@ -38,7 +38,6 @@ namespace sls {
 
     public:
         bv_plugin(context& ctx);
-        ~bv_plugin() override = default;
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h
index 395654385..fb51bc4d6 100644
--- a/src/ast/sls/sls_datatype_plugin.h
+++ b/src/ast/sls/sls_datatype_plugin.h
@@ -81,7 +81,6 @@ namespace sls {
 
     public:
         datatype_plugin(context& c);
-        ~datatype_plugin() override = default;
         family_id fid() override { return m_fid; }
         expr_ref get_value(expr* e) override;
         void initialize() override;
diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h
index 34708f3b5..45c93a8d0 100644
--- a/src/ast/sls/sls_euf_plugin.h
+++ b/src/ast/sls/sls_euf_plugin.h
@@ -60,7 +60,6 @@ namespace sls {
 
     public:
         euf_plugin(context& c);
-        ~euf_plugin() override = default;
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void start_propagation() override;
diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h
index ad29c4e9a..2b522c3fd 100644
--- a/src/ast/sls/sls_seq_plugin.h
+++ b/src/ast/sls/sls_seq_plugin.h
@@ -169,7 +169,6 @@ namespace sls {
         bool is_value(expr* e);
     public:
         seq_plugin(context& c);
-        ~seq_plugin() override = default;
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void start_propagation() override {}
diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h
index c3e6e4015..59515e9bd 100644
--- a/src/qe/mbp/mbp_euf.h
+++ b/src/qe/mbp/mbp_euf.h
@@ -21,7 +21,6 @@ namespace mbp {
         bool try_unify(term_graph& g, app* a, expr_ref_vector const& partitions, app_ref_vector& vars, vector<def>& defs);
     public:
         euf_project_plugin(ast_manager& m);
-        ~euf_project_plugin() override = default;
         
         bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
diff --git a/src/sat/sat_ddfw_wrapper.h b/src/sat/sat_ddfw_wrapper.h
index 8da7607a0..58b2aac66 100644
--- a/src/sat/sat_ddfw_wrapper.h
+++ b/src/sat/sat_ddfw_wrapper.h
@@ -37,8 +37,6 @@ namespace sat {
 
         ddfw_wrapper() {}
         
-        ~ddfw_wrapper() override = default;
-
         void set_plugin(local_search_plugin* p) { m_ddfw.set_plugin(p); }
 
         lbool check(unsigned sz, literal const* assumptions, parallel* p) override;
diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h
index dd720a6ff..510e6b8f8 100644
--- a/src/smt/theory_intblast.h
+++ b/src/smt/theory_intblast.h
@@ -50,7 +50,6 @@ namespace smt {
 
     public:
         theory_intblast(context& ctx);
-        ~theory_intblast() override = default;
 
         char const* get_name() const override { return "bv-intblast"; }
         smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index 3585db61c..2b65783b4 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -30,7 +30,6 @@ namespace smt {
         model_ref m_model;
     public:
         theory_sls(context& ctx);
-        ~theory_sls() override = default;
         model_ref get_model() { return m_model; }
         char const* get_name() const override { return "sls"; }
         smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_sls, *new_ctx); }