diff --git a/.clang-format b/.clang-format
index 7ef241e3d..c4bbbf1e1 100644
--- a/.clang-format
+++ b/.clang-format
@@ -42,6 +42,7 @@ SpaceInEmptyParentheses: false
 SpacesInCStyleCastParentheses: false
 SpacesInParentheses: false
 SpacesInSquareBrackets: false
+IndentCaseLabels: false
 
 # Alignment
 AlignConsecutiveAssignments: false
diff --git a/src/math/lp/.clang-format b/src/math/lp/.clang-format
deleted file mode 100644
index e9420012c..000000000
--- a/src/math/lp/.clang-format
+++ /dev/null
@@ -1,5 +0,0 @@
-BasedOnStyle: Google
-IndentWidth: 4
-ColumnLimit: 0
-NamespaceIndentation: All
-BreakBeforeBraces: Attach
\ No newline at end of file
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index bc498f9e4..fec10fe0e 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -211,7 +211,7 @@ struct solver::imp {
                     UNREACHABLE();
                     return l_undef;
                 }
-            for (auto const& m : m_nla_core.emons()) {
+            for (auto const &m : m_nla_core.emons()) {
                 if (!check_monic(m)) {
                     IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
                                lra.constraints().display(verbose_stream()));
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 01432cabf..4f73671ea 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3768,6 +3768,55 @@ namespace smt {
         TRACE(literal_occ, display_literal_num_occs(tout););
     }
 
+    void context::initialize_values() {
+        if (m_values.empty())
+            return;
+        expr_safe_replace sub(m);
+        for (auto const &[var, value] : m_values) {
+            initialize_value(var, value);
+            sub.insert(var, value);
+        }        
+        for (unsigned v = 0; v < get_num_bool_vars(); ++v) {
+            expr_ref var(bool_var2expr(v), m);
+            if (!var)
+                continue;
+            sub(var);
+            m_rewriter(var);
+
+            if (m.is_true(var)) {
+                m_bdata[v].m_phase_available = true;
+                m_bdata[v].m_phase = true;
+            }
+            else if (m.is_false(var)) {
+                m_bdata[v].m_phase_available = true;
+                m_bdata[v].m_phase = false;
+            } 
+        }
+
+        for (clause *cls : m_aux_clauses) {
+            literal undef_lit = null_literal;
+            bool is_true = false;
+            for (auto lit : *cls) {
+                auto v = lit.var();
+                if (m_bdata[v].m_phase_available) {
+                    bool phase = m_bdata[v].m_phase;
+                    if (lit.sign() != phase) {
+                        is_true = true;
+                        break;
+                    }
+                }
+                else {
+                    undef_lit = lit;
+                }
+            }
+            if (!is_true && undef_lit != null_literal) {
+                auto v = undef_lit.var();
+                m_bdata[v].m_phase_available = true;
+                m_bdata[v].m_phase = !undef_lit.sign();
+            }
+        }       
+    }
+
     void context::end_search() {
         m_case_split_queue->end_search_eh();
     }
@@ -3820,8 +3869,7 @@ namespace smt {
         TRACE(search, display(tout); display_enodes_lbls(tout););
         TRACE(search_detail, m_asserted_formulas.display(tout););
         init_search();
-        for (auto const& [var, value] : m_values)
-            initialize_value(var, value);
+        initialize_values();
             
         flet<bool> l(m_searching, true);
         TRACE(after_init_search, display(tout););
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 09a358e0e..7d68dc808 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -269,6 +269,7 @@ namespace smt {
         // ----------------------------------
         vector<std::pair<expr_ref, expr_ref>> m_values;
         void initialize_value(expr* var, expr* value);
+        void initialize_values();
 
 
         // -----------------------------------