diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 1cd776cc2fc..0c61bdcb201 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -223,7 +223,7 @@ class lar_solver : public column_namer {
     void insert_row_with_changed_bounds(unsigned rid);
     void detect_rows_with_changed_bounds_for_column(unsigned j);
     void detect_rows_with_changed_bounds();
-    void set_value_for_nbasic_column(unsigned j, const impq & new_val);
+
     void update_x_and_inf_costs_for_columns_with_changed_bounds();
     void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
     void solve_with_core_solver();
@@ -355,6 +355,9 @@ class lar_solver : public column_namer {
             bp.consume(a, witness);
         }
     }
+
+    void set_value_for_nbasic_column(unsigned j, const impq& new_val);
+
     // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
     constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side);
     void activate_check_on_equal(constraint_index, var_index&);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4d4c2d132f2..5505cfa7026 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2967,11 +2967,9 @@ namespace sat {
             }
             break;
         case PS_SAT_CACHING:
-            if (m_search_state == s_sat) {
-                for (unsigned i = 0; i < m_phase.size(); ++i) {
-                    m_phase[i] = m_best_phase[i];
-                }
-            }
+            if (m_search_state == s_sat) 
+                for (unsigned i = 0; i < m_phase.size(); ++i) 
+                    m_phase[i] = m_best_phase[i];                            
             break;
         case PS_RANDOM:
             for (auto& p : m_phase) p = (m_rand() % 2) == 0;