diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 504f67ad0..ed34d4a19 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -45,7 +45,7 @@ Author:
 class dependent_expr_state {
     unsigned m_qhead = 0;
     bool     m_suffix_frozen = false;
-    unsigned m_num_recfun = 0, m_num_lambdas = 0;
+    unsigned m_num_recfun = 0;
     lbool    m_has_quantifiers = l_undef;
     ast_mark m_frozen;
     func_decl_ref_vector m_frozen_trail;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 098240fc9..c23da2bba 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4672,7 +4672,6 @@ namespace smt {
             theory_id th_id     = l->get_id();
 
             for (enode * parent : enode::parents(n)) {
-                auto p = parent->get_expr();
                 family_id fid = parent->get_family_id();
                 if (fid != th_id && fid != m.get_basic_family_id()) {
                     if (is_beta_redex(parent, n))
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index 2b65783b4..856f8f3d2 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -66,7 +66,6 @@ namespace smt {
         unsigned m_final_check_ls_steps = 30000;
         unsigned m_final_check_ls_steps_delta = 10000;
         unsigned m_final_check_ls_steps_min = 10000;
-        unsigned m_final_check_ls_steps_max = 30000;
         bool     m_has_unassigned_clause_after_resolve = false;
         unsigned m_after_resolve_decide_gap = 4;
         unsigned m_after_resolve_decide_count = 0;
diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index ebae4cb57..dffb5f15c 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -460,7 +460,6 @@ class parallel_solver {
         };
 
         unsigned         id;
-        parallel_solver& p;
         batch_manager&   b;
         ast_manager      m;                 /* worker-local manager */
         ref<solver>      s;                 /* translated solver copy */
@@ -579,7 +578,7 @@ class parallel_solver {
         worker(unsigned id, parallel_solver& p,
                solver& src, params_ref const& params,
                expr_ref_vector const& src_asms)
-            : id(id), p(p), b(p.m_batch_manager),
+            : id(id), b(p.m_batch_manager),
               asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager())
         {
             /* create translated solver copy */