diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index e79c64755..6d790b68d 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -348,7 +348,6 @@ namespace smt {
                     expr_ref le(m_arith.mk_le(set_sz->get_arg(1), m_arith.mk_int(0)), m);
                     literal le_lit = mk_literal(le);
                     literal sz_lit = mk_literal(set_sz);
-                    unsigned k = i.m_selects.size();
                     for (unsigned k = i.m_selects.size(); rational(k) < i.m_size; ++k) {
                         expr_ref idx = mk_index_skolem(set_sz, set, k);
                         app_ref sel(mk_select(set, idx), m);
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index bad35fa3e..53a3c4a24 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -154,7 +154,6 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) {
 
 lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
     bool models_enabled = g->models_enabled();
-    bool proofs_enabled = g->proofs_enabled();
     bool cores_enabled  = g->unsat_core_enabled();
     md   = nullptr;
     pr   = nullptr;