diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 2fccf4877..ace89c04d 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -670,10 +670,11 @@ namespace sat {
         }
     }
 
-    void local_search::set_phase(bool_var v, bool f) {
+    void local_search::set_phase(bool_var v, lbool f) {
         unsigned& bias = m_vars[v].m_bias;
-        if (f && bias < 100) bias++;
-        if (!f && bias > 0) bias--;
+        if (f == l_true && bias < 100) bias++;
+        if (f == l_false && bias > 0) bias--;
+        // f == l_undef ?
     }
 
 }
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 75bfdbb54..03206eb60 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -225,7 +225,7 @@ namespace sat {
 
         unsigned num_vars() const { return m_vars.size() - 1; }     // var index from 1 to num_vars
 
-        void set_phase(bool_var v, bool f);
+        void set_phase(bool_var v, lbool f);
 
         bool get_phase(bool_var v) const { return is_true(v); }
 
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index 55c9d8125..4eb247fc0 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -210,20 +210,21 @@ namespace sat {
 
     void parallel::_set_phase(solver& s) {
         if (!m_phase.empty()) {
-            m_phase.reserve(s.num_vars(), 0);
+            m_phase.reserve(s.num_vars(), l_undef);
             for (unsigned i = 0; i < s.num_vars(); ++i) {
                 if (s.value(i) != l_undef) {
-                    m_phase[i] += (s.value(i) == l_true) ? 1 : -1;
+                    m_phase[i] = s.value(i);
                     continue;
                 }
                 switch (s.m_phase[i]) {
                 case POS_PHASE:
-                    m_phase[i]++;
+                    m_phase[i] = l_true;
                     break;
                 case NEG_PHASE:
-                    m_phase[i]--;
+                    m_phase[i] = l_false;
                     break;
                 default:
+                    m_phase[i] = l_undef;
                     break;
                 }
             }
@@ -246,39 +247,33 @@ namespace sat {
 
     void parallel::_get_phase(solver& s) {
         if (!m_phase.empty()) {
-            m_phase.reserve(s.num_vars(), 0);
+            m_phase.reserve(s.num_vars(), l_undef);
             for (unsigned i = 0; i < s.num_vars(); ++i) {
-                if (m_phase[i] < 0) {
-                    s.m_phase[i] = NEG_PHASE;
-                }
-                else if (m_phase[i] > 0) {
-                    s.m_phase[i] = POS_PHASE;
+                switch (m_phase[i]) {
+                case l_false: s.m_phase[i] = NEG_PHASE; break;
+                case l_true: s.m_phase[i] = POS_PHASE; break;
+                default: break;
                 }
             }
         }
     }
 
-    void parallel::get_phase(local_search& s) {
+   void parallel::get_phase(local_search& s) {
         #pragma omp critical (par_solver)
         {
             for (unsigned i = 0; i < m_phase.size(); ++i) {
-                if (m_phase[i] < 0) {
-                    s.set_phase(i, false);
-                }
-                else if (m_phase[i] > 0) {
-                    s.set_phase(i, true);
-                }
+                s.set_phase(i, m_phase[i]);
             }
-            m_phase.reserve(s.num_vars(), 0);
+            m_phase.reserve(s.num_vars(), l_undef);
         }
     }
 
     void parallel::set_phase(local_search& s) {
         #pragma omp critical (par_solver)
         {
-            m_phase.reserve(s.num_vars(), 0);
+            m_phase.reserve(s.num_vars(), l_undef);
             for (unsigned i = 0; i < s.num_vars(); ++i) {
-                m_phase[i] += (s.get_phase(i) ? 1 : -1);
+                m_phase[i] = s.get_phase(i) ? l_true : l_false;
             }
         }
     }
diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h
index cb68dd0f9..4d8e4a82d 100644
--- a/src/sat/sat_parallel.h
+++ b/src/sat/sat_parallel.h
@@ -60,7 +60,7 @@ namespace sat {
         index_set      m_unit_set;
         literal_vector m_lits;
         vector_pool    m_pool;
-        int_vector     m_phase;
+        svector<lbool> m_phase;
 
         scoped_limits      m_scoped_rlimit;
         vector<reslimit>   m_limits;