diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index ab29ab7f4..1bd3f1c3d 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -44,10 +44,6 @@ class int_solver {
         int_solver&         lia;
         lar_solver&         lra;
         lar_core_solver&    lrac;
-        unsigned            m_patch_success = 0;
-        unsigned            m_patch_fail = 0;
-        unsigned            m_num_ones = 0;
-        unsigned            m_num_divides = 0;
     public:
         patcher(int_solver& lia);
         bool should_apply() const { return true; }
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index bf27777c4..5cb3729ab 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -194,7 +194,6 @@ namespace smt {
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
             m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
-        static unsigned s_count = 0;
         
         if (m_has_log) {
             init_pp_out();