diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 95b043bd7..c96096c65 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -89,6 +89,7 @@ public:
     ~re2automaton();
     eautomaton* operator()(expr* e);
     void set_solver(expr_solver* solver);
+    bool has_solver() const { return m_solver; }
     eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
 };
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 95f804863..b704795b2 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -238,8 +238,7 @@ theory_seq::~theory_seq() {
 }
 
 void theory_seq::init(context* ctx) {
-    theory::init(ctx);
-    m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
+    theory::init(ctx);    
 }
 
 final_check_status theory_seq::final_check_eh() {
@@ -4168,6 +4167,9 @@ eautomaton* theory_seq::get_automaton(expr* re) {
     if (m_re2aut.find(re, result)) {
         return result;
     }
+    if (!m_mk_aut.has_solver()) {
+        m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
+    }
     result = m_mk_aut(re);
     if (result) {
         display_expr disp(m);
diff --git a/src/test/get_implied_equalities.cpp b/src/test/get_implied_equalities.cpp
index 952fb121a..dae182a34 100644
--- a/src/test/get_implied_equalities.cpp
+++ b/src/test/get_implied_equalities.cpp
@@ -75,9 +75,9 @@ static void tst_get_implied_equalities1() {
 }
 
 static void tst_get_implied_equalities2() {
-    enable_trace("after_search");
-    enable_trace("get_implied_equalities");
-    enable_trace("implied_equalities");
+    //enable_trace("after_search");
+    //enable_trace("get_implied_equalities");
+    //enable_trace("implied_equalities");
     Z3_config cfg = Z3_mk_config();
     Z3_context ctx = Z3_mk_context(cfg);
     Z3_del_config(cfg);
diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp
index 4828046be..1116c5420 100644
--- a/src/test/sat_local_search.cpp
+++ b/src/test/sat_local_search.cpp
@@ -7,7 +7,6 @@
 static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
 {
     char  line[16383];
-    int   cur_term;
     // for temperally storage
 
     std::ifstream infile(filename);
@@ -18,6 +17,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
     }
     infile.getline(line, 16383);
 #ifdef _WINDOWS
+    int cur_term;
     int num_vars = 0, num_constraints = 0;
     sscanf_s(line, "%d %d", &num_vars, &num_constraints);
     //std::cout << "number of variables: " << num_vars << '\n';