diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 76de2d0e7..8cb5ff480 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -259,6 +259,7 @@ namespace sat {
         bool get_phase(bool_var v) const { return is_true(v); }
 
         model& get_model() { return m_model; }
+
     };
 }
 
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 3356763c0..77e562384 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -710,11 +710,11 @@ namespace sat {
             m_watches.push_back(watch_list());
             m_bstamp.push_back(0);
             m_bstamp.push_back(0);
+            m_dfs.push_back(dfs_info());
+            m_dfs.push_back(dfs_info());
+            m_lits.push_back(lit_info());
+            m_lits.push_back(lit_info());
             m_rating.push_back(0);
-            m_dfs.push_back(dfs_info());
-            m_dfs.push_back(dfs_info());
-            m_lits.push_back(lit_info());
-            m_lits.push_back(lit_info());
             m_prefix.push_back(prefix());
             m_freevars.insert(v);
         }
@@ -1125,6 +1125,7 @@ namespace sat {
         unsigned scope_lvl() const { return m_trail_lim.size(); }
 
         void assign(literal l) {
+            SASSERT(m_level > 0);
             if (is_undef(l)) {
                 set_true(l);
                 m_trail.push_back(l);
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index 6652bfc3e..67d446a29 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -91,7 +91,7 @@ namespace sat {
         return false;
     }
 
-    parallel::parallel(solver& s): m_scoped_rlimit(s.rlimit()) {}
+    parallel::parallel(solver& s): m_scoped_rlimit(s.rlimit()), m_num_clauses(0) {}
 
     parallel::~parallel() {
         for (unsigned i = 0; i < m_solvers.size(); ++i) {            
@@ -227,9 +227,11 @@ namespace sat {
             }
             if (90 * m_num_clauses > 100 * s.m_clauses.size() && !m_solver_copy) {
                 // time to update local search with new clauses.
+                // there could be multiple local search engines runing at the same time.
                 IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh local search " << m_num_clauses << " -> " << s.m_clauses.size() << ")\n";);
                 m_solver_copy = alloc(solver, s.m_params, s.rlimit());
                 m_solver_copy->copy(s);
+                m_num_clauses = s.m_clauses.size();
             }
         }
     }
@@ -264,16 +266,20 @@ namespace sat {
    void parallel::get_phase(local_search& s) {
         #pragma omp critical (par_solver)
         {
-            if (m_solver_copy) {
+            if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
                 s.import(*m_solver_copy.get(), true);
+                m_num_clauses = s.num_non_binary_clauses();
+                SASSERT(s.num_non_binary_clauses() == m_solver_copy->m_clauses.size());
                 m_solver_copy = 0;
             }
+            if (m_num_clauses < s.num_non_binary_clauses()) {
+                m_num_clauses = s.num_non_binary_clauses();
+            }
             for (unsigned i = 0; i < m_phase.size(); ++i) {
                 s.set_phase(i, m_phase[i]);
                 m_phase[i] = l_undef;
             }
             m_phase.reserve(s.num_vars(), l_undef);
-            m_num_clauses = s.num_non_binary_clauses();
         }
     }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 539699382..bddf551df 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -863,7 +863,7 @@ namespace sat {
         int num_local_search  = static_cast<int>(m_config.m_local_search);
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
-            l->config().set_seed(m_config.m_random_seed);
+            l->config().set_seed(m_config.m_random_seed + i);
             l->import(*this, false);
             ls.push_back(l);
         }