diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index ec4f14c90..4f48f20f2 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -327,7 +327,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
     if (!offset || (a.is_numeral(offset, r) && r.is_zero())) {
         // |s| = 0 => indexof(t,s,0) = 0
         add_axiom(~s_eq_empty, i_eq_0);
-#if 0
+#if 1
         expr_ref x  = m_sk.mk_indexof_left(t, s);
         expr_ref y  = m_sk.mk_indexof_right(t, s);
         xsy         = mk_concat(x, s, y);
diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index f367e5bba..9e4bd2179 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -95,7 +95,6 @@ collect_induction_literals::collect_induction_literals(context& ctx, ast_manager
     vs(vs),
     m_literal_index(0)
 {
-//    (void)vs;
 }
     
 literal_vector collect_induction_literals::operator()() {    
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index e113e4ed0..1ab44c1f6 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3565,7 +3565,6 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
     if (k_min < UINT_MAX) {
         m_max_unfolding_depth++;
         k_min *= 2;
-        rational lo;
         if (m_util.is_seq(s_min))
             k_min = std::max(m_util.str.min_length(s_min), k_min);
         IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");