diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h
index df1dc00f1..6f471f58e 100644
--- a/src/sat/smt/arith_proof_checker.h
+++ b/src/sat/smt/arith_proof_checker.h
@@ -303,8 +303,6 @@ namespace arith {
             m_implied_eq("implied-eq"), 
             m_bound("bound") {}
 
-        ~proof_checker() override {}
-        
         void reset() {
             m_ineq.reset();
             m_conseq.reset();
diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h
index 479ad2933..17c7404f2 100644
--- a/src/sat/smt/euf_ackerman.h
+++ b/src/sat/smt/euf_ackerman.h
@@ -29,12 +29,12 @@ namespace euf {
     class ackerman {
 
         struct inference : dll_base<inference>{
-            bool is_cc;
             expr* a, *b, *c;
             unsigned   m_count{ 0 };
-            inference():is_cc(false), a(nullptr), b(nullptr), c(nullptr) {}
-            inference(app* a, app* b):is_cc(true), a(a), b(b), c(nullptr) {}
-            inference(expr* a, expr* b, expr* c):is_cc(false), a(a), b(b), c(c) {}
+            bool is_cc;
+            inference(): a(nullptr), b(nullptr), c(nullptr), is_cc(false) {}
+            inference(app* a, app* b): a(a), b(b), c(nullptr), is_cc(true) {}
+            inference(expr* a, expr* b, expr* c): a(a), b(b), c(c), is_cc(false) {}
         };
 
         struct inference_eq {
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 5061ad88c..f432443e9 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -23,7 +23,6 @@ Author:
 #include "sat/smt/arith_proof_checker.h"
 #include "sat/smt/q_proof_checker.h"
 #include "sat/smt/tseitin_proof_checker.h"
-#include <iostream>
 
 namespace euf {
 
@@ -121,8 +120,6 @@ namespace euf {
     public:
         eq_proof_checker(ast_manager& m): m(m) {}
 
-        ~eq_proof_checker() override {}
-
         expr_ref_vector clause(app* jst) override {
             expr_ref_vector result(m);
             for (expr* arg : *jst) 
@@ -213,8 +210,6 @@ namespace euf {
 
     public:
         res_proof_checker(ast_manager& m, proof_checker& pc): m(m), pc(pc) {}
-        
-        ~res_proof_checker() override {}
 
         bool check(app* jst) override {
             if (jst->get_num_args() != 3)
diff --git a/src/sat/smt/euf_proof_checker.h b/src/sat/smt/euf_proof_checker.h
index 0d3dbcb9e..8b1b5d671 100644
--- a/src/sat/smt/euf_proof_checker.h
+++ b/src/sat/smt/euf_proof_checker.h
@@ -60,7 +60,6 @@ namespace euf {
         symbol m_rule;
     public:
         smt_proof_checker_plugin(ast_manager& m, symbol const& n): m(m), m_rule(n) {}
-        ~smt_proof_checker_plugin() override {}
         bool check(app* jst) override { return false; }
         expr_ref_vector clause(app* jst) override;        
         void register_plugins(proof_checker& pc) override { pc.register_plugin(m_rule, this); }
diff --git a/src/sat/smt/q_proof_checker.h b/src/sat/smt/q_proof_checker.h
index 6b309d1c6..4072739c7 100644
--- a/src/sat/smt/q_proof_checker.h
+++ b/src/sat/smt/q_proof_checker.h
@@ -42,8 +42,6 @@ namespace q {
             m_inst("inst"),
             m_bind("bind") {
             }
-
-        ~proof_checker() override {}
         
         expr_ref_vector clause(app* jst) override;
 
diff --git a/src/sat/smt/tseitin_proof_checker.h b/src/sat/smt/tseitin_proof_checker.h
index 677eabfa4..86a109ed8 100644
--- a/src/sat/smt/tseitin_proof_checker.h
+++ b/src/sat/smt/tseitin_proof_checker.h
@@ -61,8 +61,6 @@ namespace tseitin {
             m(m) {
         }
 
-        ~proof_checker() override {}
-        
         expr_ref_vector clause(app* jst) override;
         
         bool check(app* jst) override;