From 97bf2a514588f01e377f5e546ebe56a9d1f53a36 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sun, 1 Feb 2026 15:22:58 -0800
Subject: [PATCH] Remove redundant non-virtual destructors with = default
 (#8462)

* Initial plan

* Remove 6 non-virtual destructors with no code (= default)

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
---
 src/ast/sls/sat_ddfw.h                  | 2 --
 src/ast/sls/sls_smt_solver.h            | 1 -
 src/math/lp/lar_term.h                  | 1 -
 src/smt/arith_eq_solver.h               | 1 -
 src/solver/preferred_value_propagator.h | 1 -
 src/util/dlist.h                        | 1 -
 6 files changed, 7 deletions(-)

diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index 4bf52cf16..f7cfb2dca 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -226,8 +226,6 @@ namespace sat {
 
         ddfw() {}
 
-        ~ddfw() = default;
-
         void set_plugin(local_search_plugin* p) { m_plugin = p; }
 
         lbool check(unsigned sz, literal const* assumptions);
diff --git a/src/ast/sls/sls_smt_solver.h b/src/ast/sls/sls_smt_solver.h
index 6f24b708d..26a10704b 100644
--- a/src/ast/sls/sls_smt_solver.h
+++ b/src/ast/sls/sls_smt_solver.h
@@ -32,7 +32,6 @@ namespace sls {
         
     public:
         smt_solver(ast_manager& m, params_ref const& p);
-        ~smt_solver() = default;
         void assert_expr(expr* e);
         lbool check();
         model_ref get_model();
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index d60d84f55..cca541801 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -99,7 +99,6 @@ public:
     lar_term& operator=(const lar_term& other) = default;
     // move assignment operator
     lar_term& operator=(lar_term&& other) noexcept = default;
-    ~lar_term() = default;
     lar_term(const lar_term& a) {
         for (auto const& p : a) {
             add_monomial(p.coeff(), p.var());
diff --git a/src/smt/arith_eq_solver.h b/src/smt/arith_eq_solver.h
index 00256f0f2..405cd1177 100644
--- a/src/smt/arith_eq_solver.h
+++ b/src/smt/arith_eq_solver.h
@@ -62,7 +62,6 @@ class arith_eq_solver {
 
 public:
     arith_eq_solver(ast_manager & m, params_ref const& p = params_ref());
-    ~arith_eq_solver() = default;
 
     // Integer linear solver for a single equation.
     // The array values contains integer coefficients
diff --git a/src/solver/preferred_value_propagator.h b/src/solver/preferred_value_propagator.h
index da83c1fa3..8ff05bff6 100644
--- a/src/solver/preferred_value_propagator.h
+++ b/src/solver/preferred_value_propagator.h
@@ -66,7 +66,6 @@ public:
             return p.decide(*cb);
         };
     }
-    ~preferred_value_propagator() = default;
     void set_preferred(expr *e) {
         m_preferred.push_back(e);
         if (m_trail.get_num_scopes() > 0)
diff --git a/src/util/dlist.h b/src/util/dlist.h
index cd4113457..1998dce1d 100644
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@@ -32,7 +32,6 @@ class dll_base {
 
 protected:
     dll_base() = default;
-    ~dll_base() = default;
 
 public:
     dll_base(dll_base const&) = delete;