diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index d484ecda4..68e18375f 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -460,7 +460,6 @@ struct goal2sat::imp {
         check_unsigned(k);                
         svector<wliteral> wlits;
         convert_pb_args(t, wlits);
-        unsigned sz = m_result_stack.size();
         if (root && m_solver.num_user_scopes() == 0) {
             m_result_stack.reset();
             unsigned k1 = k.get_unsigned();
@@ -492,7 +491,6 @@ struct goal2sat::imp {
             k += rational(wl.first);
         }
         check_unsigned(k);
-        unsigned sz = m_result_stack.size();
         if (root && m_solver.num_user_scopes() == 0) {
             m_result_stack.reset();
             unsigned k1 = k.get_unsigned();
@@ -550,7 +548,6 @@ struct goal2sat::imp {
     void convert_at_least_k(app* t, rational const& k, bool root, bool sign) {
         SASSERT(k.is_unsigned());
         sat::literal_vector lits;
-        unsigned sz = m_result_stack.size();
         convert_pb_args(t->get_num_args(), lits);
         if (root && m_solver.num_user_scopes() == 0) {
             m_result_stack.reset();
@@ -570,7 +567,6 @@ struct goal2sat::imp {
     void convert_at_most_k(app* t, rational const& k, bool root, bool sign) {
         SASSERT(k.is_unsigned());
         sat::literal_vector lits;
-        unsigned sz = m_result_stack.size();
         convert_pb_args(t->get_num_args(), lits);
         for (sat::literal& l : lits) {
             l.neg();
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 730061c8b..2d894d3ee 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -293,13 +293,6 @@ static tactic * mk_seq_smt_tactic(params_ref const & p) {
     return alloc(smt_tactic, p);
 }
 
-static tactic * mk_seq_smt_tactic_using(bool auto_config, params_ref const & _p) {
-    params_ref p = _p;
-    p.set_bool("auto_config", auto_config);
-    tactic * r = mk_seq_smt_tactic(p);
-    TRACE("smt_tactic", tout << "auto_config: " << auto_config << "\nr: " << r << "\np: " << p << "\n";);
-    return using_params(r, p);
-}
 
 tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
     return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);