diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index 4f48f20f2..ec4f14c90 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 1
+#if 0
         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 dc90b1047..f367e5bba 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -95,7 +95,7 @@ collect_induction_literals::collect_induction_literals(context& ctx, ast_manager
     vs(vs),
     m_literal_index(0)
 {
-    (void)vs;
+//    (void)vs;
 }
     
 literal_vector collect_induction_literals::operator()() {    
@@ -538,10 +538,9 @@ void induction_lemmas::apply_induction(literal lit, induction_positions_t const
     }
 }
 
-induction_lemmas::induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs):
+induction_lemmas::induction_lemmas(context& ctx, ast_manager& m):
     ctx(ctx),
     m(m),
-    vs(vs),
     m_dt(m),
     m_a(m),
     m_rec(m),
@@ -554,7 +553,7 @@ induction::induction(context& ctx, ast_manager& m):
     m(m),
     vs(m),
     m_collect_literals(ctx, m, vs),
-    m_create_lemmas(ctx, m, vs)
+    m_create_lemmas(ctx, m)
 {}
 
 // TBD: use smt_arith_value to also include state from arithmetic solver
diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h
index 60e428cf8..8db1a99ab 100644
--- a/src/smt/smt_induction.h
+++ b/src/smt/smt_induction.h
@@ -91,7 +91,6 @@ namespace smt {
 
         context&       ctx;
         ast_manager&   m;
-        value_sweep&   vs;
         datatype::util m_dt;
         arith_util     m_a;
         recfun::util   m_rec;
@@ -123,7 +122,7 @@ namespace smt {
         void apply_induction(literal lit, induction_positions_t const & positions);
 
     public:
-        induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs);
+        induction_lemmas(context& ctx, ast_manager& m);
 
         bool operator()(literal lit);
     };
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 1ab44c1f6..e113e4ed0 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3565,6 +3565,7 @@ 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");