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;