diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index bfae22f21..0008a0ee9 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -19,7 +19,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "util/vector.h"
diff --git a/src/math/lp/column_info.h b/src/math/lp/column_info.h
index c0b09e21f..1dc0c60c7 100644
--- a/src/math/lp/column_info.h
+++ b/src/math/lp/column_info.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/column_namer.h b/src/math/lp/column_namer.h
index ccd3cffad..cef58ed21 100644
--- a/src/math/lp/column_namer.h
+++ b/src/math/lp/column_namer.h
@@ -18,7 +18,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <string>
 #include "math/lp/static_matrix.h"
 namespace lp {
diff --git a/src/math/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp
index e1ce8fb1b..18bef8303 100644
--- a/src/math/lp/core_solver_pretty_printer.cpp
+++ b/src/math/lp/core_solver_pretty_printer.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include "math/lp/numeric_pair.h"
 #include "math/lp/core_solver_pretty_printer_def.h"
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h
index 46e9ebf7e..5bf29d511 100644
--- a/src/math/lp/core_solver_pretty_printer.h
+++ b/src/math/lp/core_solver_pretty_printer.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include <limits>
 #include <string>
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index 17f82af9c..b8048b241 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <limits>
diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 9633e2dab..a39ef5ef9 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include <functional>
 #include "math/lp/nex.h"
diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h
index 986a2d20e..e850a9acd 100644
--- a/src/math/lp/dense_matrix_def.h
+++ b/src/math/lp/dense_matrix_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/lp_settings.h"
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index e5da7c702..bcdb81dd8 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -18,7 +18,6 @@
   replaced rooted_mons.h and rooted_mon, rooted_mon_tabled
 
 --*/
-// clang-format off
 
 #include "math/lp/emonics.h"
 #include "math/lp/nla_defs.h"
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 8f0f33175..e4f4f4848 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -18,7 +18,6 @@
     to replace rooted_mons.h and rooted_mon, rooted_mon_tabled
 
   --*/
-// clang-format off
 
 #pragma once
 #include "math/lp/lp_utils.h"
diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h
index 67df7bab9..b7f721a30 100644
--- a/src/math/lp/explanation.h
+++ b/src/math/lp/explanation.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/lp_utils.h"
 #include "util/map.h"
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index aad52c58e..b233894ad 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -18,7 +18,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/monic.h"
diff --git a/src/math/lp/factorization_factory_imp.cpp b/src/math/lp/factorization_factory_imp.cpp
index 1406d5864..ace85a050 100644
--- a/src/math/lp/factorization_factory_imp.cpp
+++ b/src/math/lp/factorization_factory_imp.cpp
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #include "math/lp/factorization_factory_imp.h"
 #include "math/lp/nla_core.h"
 namespace nla {
diff --git a/src/math/lp/factorization_factory_imp.h b/src/math/lp/factorization_factory_imp.h
index 7c76299dc..599039094 100644
--- a/src/math/lp/factorization_factory_imp.h
+++ b/src/math/lp/factorization_factory_imp.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 namespace nla {
diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h
index 0fc9c404b..a4f6693a2 100644
--- a/src/math/lp/general_matrix.h
+++ b/src/math/lp/general_matrix.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include <functional>
 namespace lp {
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index babb10d72..2ecbc49ac 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #include "math/lp/gomory.h"
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h
index acca900df..68e42feb9 100644
--- a/src/math/lp/gomory.h
+++ b/src/math/lp/gomory.h
@@ -15,7 +15,6 @@ Author:
 
 Revision History:
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/lar_term.h"
 #include "math/lp/lia_move.h"
diff --git a/src/math/lp/hnf.h b/src/math/lp/hnf.h
index 53b33b37a..75a69393f 100644
--- a/src/math/lp/hnf.h
+++ b/src/math/lp/hnf.h
@@ -26,7 +26,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/numeric_pair.h"
 #include "util/ext_gcd.h"
diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
index e2fd85866..3c4ea10ab 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -9,7 +9,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/hnf_cutter.h"
diff --git a/src/math/lp/hnf_cutter.h b/src/math/lp/hnf_cutter.h
index 98f9770e8..b3530ea29 100644
--- a/src/math/lp/hnf_cutter.h
+++ b/src/math/lp/hnf_cutter.h
@@ -14,7 +14,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 
 #pragma once
 #include "math/lp/lar_term.h"
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 3b4cce827..4d4ac4975 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 
 #include "math/lp/horner.h"
 #include "math/lp/nla_core.h"
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index ce630b0c2..2b6fc3cd8 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"
diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h
index 239103035..9435edcdc 100644
--- a/src/math/lp/implied_bound.h
+++ b/src/math/lp/implied_bound.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "math/lp/lar_constraints.h"
diff --git a/src/math/lp/incremental_vector.h b/src/math/lp/incremental_vector.h
index f124eb05e..0bb2829eb 100644
--- a/src/math/lp/incremental_vector.h
+++ b/src/math/lp/incremental_vector.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h
index aab13fc9c..92d8f2adf 100644
--- a/src/math/lp/indexed_value.h
+++ b/src/math/lp/indexed_value.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 namespace lp {
diff --git a/src/math/lp/indexed_vector.cpp b/src/math/lp/indexed_vector.cpp
index f5c34e1f9..fe0892541 100644
--- a/src/math/lp/indexed_vector.cpp
+++ b/src/math/lp/indexed_vector.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include "util/vector.h"
 #include "math/lp/indexed_vector_def.h"
 namespace lp {
diff --git a/src/math/lp/indexed_vector.h b/src/math/lp/indexed_vector.h
index b5f5e6cb8..9f3119e9a 100644
--- a/src/math/lp/indexed_vector.h
+++ b/src/math/lp/indexed_vector.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h
index c6f530d99..034325088 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "util/vector.h"
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index 47a9ddcbe..4bfe2b827 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -15,7 +15,6 @@
 
   Revision History:
   --*/
-// clang-format off
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/int_branch.h"
diff --git a/src/math/lp/int_branch.h b/src/math/lp/int_branch.h
index 6943bede5..9601cb65e 100644
--- a/src/math/lp/int_branch.h
+++ b/src/math/lp/int_branch.h
@@ -15,7 +15,6 @@ Author:
 
 Revision History:
 --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index 787b82da7..da724a543 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -15,7 +15,6 @@ Author:
 
 Revision History:
 --*/
-// clang-format off
 
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/int_cube.h b/src/math/lp/int_cube.h
index 9ac6773ab..4addc096b 100644
--- a/src/math/lp/int_cube.h
+++ b/src/math/lp/int_cube.h
@@ -19,7 +19,6 @@ Author:
 
 Revision History:
 --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/lia_move.h"
diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp
index e243783cc..4801cc436 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -45,7 +45,6 @@ Accumulative:
  
 
 --*/
-// clang-format off
 
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h
index b77179409..28ac2f7b3 100644
--- a/src/math/lp/int_gcd_test.h
+++ b/src/math/lp/int_gcd_test.h
@@ -24,7 +24,6 @@ Author:
 
 Revision History:
 --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/lia_move.h"
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 16fc2b1a3..88a31e65d 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -2,7 +2,6 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-// clang-format off
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/lp_utils.h"
@@ -138,8 +137,7 @@ namespace lp {
                    try_patch_column(v, c.var(), delta_plus);
         }
     }
-    // clang-format off
-    
+        
     bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
         const auto & A = lra.A_r();
         if (delta < 0) {
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index fad040965..4c9f43ffe 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "math/lp/static_matrix.h"
diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
index 3bb6e7882..f8cffbe57 100644
--- a/src/math/lp/lar_constraints.h
+++ b/src/math/lp/lar_constraints.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include <utility>
diff --git a/src/math/lp/lar_core_solver.cpp b/src/math/lp/lar_core_solver.cpp
index bdb89f76b..09d01f4cc 100644
--- a/src/math/lp/lar_core_solver.cpp
+++ b/src/math/lp/lar_core_solver.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <utility>
 #include <memory>
 #include <string>
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index a67eb4d48..5d445105f 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -5,7 +5,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <string>
@@ -17,7 +16,6 @@ Author:
 #include "math/lp/stacked_vector.h"
 #include "util/stacked_value.h"
 namespace lp {
-// clang-format off
 class lar_core_solver  {
     vector<std::pair<mpq, unsigned>> m_infeasible_linear_combination;
     int m_infeasible_sum_sign; // todo: get rid of this field
diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h
index 3f7866717..942c87b3b 100644
--- a/src/math/lp/lar_core_solver_def.h
+++ b/src/math/lp/lar_core_solver_def.h
@@ -9,7 +9,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <string>
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 0ad3420b9..d1a9ece86 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2,7 +2,6 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Nikolaj Bjorner, Lev Nachmanson
 */
-// clang-format off
 #include "math/lp/lar_solver.h"
 #include "smt/params/smt_params_helper.hpp"
 
@@ -696,7 +695,6 @@ namespace lp {
         }
     }
 
-    void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
         if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) 
             insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]);
         else 
@@ -1753,8 +1751,7 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
-        lconstraint_kind kind,
-        const mpq& right_side,
+                const mpq& right_side,
         constraint_index constr_index,
         unsigned& equal_to_j) {
         update_column_type_and_bound(j, kind, right_side, constr_index);
@@ -1897,8 +1894,7 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
-        lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
-        lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
+                lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
 
         mpq y_of_bound(0);
         switch (kind) {
@@ -1946,8 +1942,7 @@ namespace lp {
     }
     // clang-format off
     void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
-        lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
-        lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
+                lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
         mpq y_of_bound(0);
         switch (kind) {
         case LT:
@@ -2033,8 +2028,7 @@ namespace lp {
     }
     // clang-format off
     bool lar_solver::column_corresponds_to_term(unsigned j) const {
-        return tv::is_term(m_var_register.local_to_external(j));
-    }
+            }
 
     var_index lar_solver::to_column(unsigned ext_j) const {
         return m_var_register.external_to_local(ext_j);
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index b130c198e..75fb4338c 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include <algorithm>
 #include <functional>
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index 65262d5dd..fc73f949f 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include "math/lp/indexed_vector.h"
 #include "util/map.h"
diff --git a/src/math/lp/lia_move.h b/src/math/lp/lia_move.h
index b1505dbc9..ca61d7b7a 100644
--- a/src/math/lp/lia_move.h
+++ b/src/math/lp/lia_move.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 namespace lp {
 enum class lia_move {
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
index 9d0bd2476..2a4e5058d 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -7,7 +7,6 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 #pragma once
 
 #include "util/inf_rational.h"
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index a909e8472..da2e4488d 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -4,7 +4,6 @@
   Nikolaj Bjorner (nbjorner)
   Lev Nachmanson   (levnach)
 */
-//clang-format off
 #pragma once
 #include <utility>
 
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
index 1859630e4..28f92d8e2 100644
--- a/src/math/lp/lp_core_solver_base.cpp
+++ b/src/math/lp/lp_core_solver_base.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <utility>
 #include <memory>
 #include <string>
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 47e09a4c8..15449f92f 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include <set>
 #include "util/vector.h"
@@ -291,8 +290,8 @@ public:
     X bound_span(unsigned j) const {
         return m_upper_bounds[j] - m_lower_bounds[j];
     }
-
-    std::string column_name(unsigned column) const;
+        // clang-format on       
+        std::string column_name(unsigned column) const;
 
     bool make_column_feasible(unsigned j, numeric_pair<mpq> & delta) {
         bool ret = false;
@@ -303,7 +302,7 @@ public:
             lp_assert(m_lower_bounds[j] == m_upper_bounds[j]);
             if (x != m_lower_bounds[j]) {
                 delta = m_lower_bounds[j] - x;
-                ret = true;;
+                ret = true;
             }
             break;
         case column_type::boxed:
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 756ff9af3..319966091 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <set>
diff --git a/src/math/lp/lp_primal_core_solver.cpp b/src/math/lp/lp_primal_core_solver.cpp
index 0698c9962..efbfd27e1 100644
--- a/src/math/lp/lp_primal_core_solver.cpp
+++ b/src/math/lp/lp_primal_core_solver.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <utility>
 #include <memory>
 #include <string>
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 79e0d7590..d4130faae 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/core_solver_pretty_printer.h"
 #include "math/lp/lp_core_solver_base.h"
@@ -159,8 +158,7 @@ namespace lp {
     }
     return r;
   }
-    // clang-format off
-    int find_beneficial_entering_in_row_tableau_rows_bland_mode(int i, T &a_ent) {
+        int find_beneficial_entering_in_row_tableau_rows_bland_mode(int i, T &a_ent) {
         int j = -1;
         unsigned bj = this->m_basis[i];
         bool bj_needs_to_grow = needs_to_grow(bj);
@@ -183,8 +181,7 @@ namespace lp {
             m_inf_row_index_for_tableau = i;
         return j;
     }
-    //clang-format off
-    int find_beneficial_entering_tableau_rows(int i, T &a_ent) {
+        int find_beneficial_entering_tableau_rows(int i, T &a_ent) {
         if (m_bland_mode_tableau)
             return find_beneficial_entering_in_row_tableau_rows_bland_mode(i, a_ent);
         // a short row produces short infeasibility explanation and benefits at
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 909dfd086..e18a5ef05 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <list>
diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h
index 905bbba3c..dbcced4ab 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 // this is a part of lp_primal_core_solver that deals with the tableau
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index 723a4ba2d..b72b837fd 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include "smt/params/smt_params_helper.hpp"
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 4e03007bb..727bc3531 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h
index 12c53551f..a19558949 100644
--- a/src/math/lp/lp_settings_def.h
+++ b/src/math/lp/lp_settings_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <cmath>
diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h
index 6f1f2e3d4..ac046e1a1 100644
--- a/src/math/lp/lp_types.h
+++ b/src/math/lp/lp_types.h
@@ -17,11 +17,9 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <sstream>
-// clang-format off
 #include <limits.h>
 #include "util/debug.h"
 namespace nla {
diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h
index 3a796c42b..3c1383cb3 100644
--- a/src/math/lp/lp_utils.h
+++ b/src/math/lp/lp_utils.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include <string>
 #include "math/lp/numeric_pair.h"
diff --git a/src/math/lp/matrix.cpp b/src/math/lp/matrix.cpp
index 1176a6358..1ea2da263 100644
--- a/src/math/lp/matrix.cpp
+++ b/src/math/lp/matrix.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include "math/lp/lp_settings.h"
 #include "math/lp/matrix_def.h"
 #include "math/lp/static_matrix.h"
diff --git a/src/math/lp/matrix.h b/src/math/lp/matrix.h
index 306f43a57..88a405614 100644
--- a/src/math/lp/matrix.h
+++ b/src/math/lp/matrix.h
@@ -6,7 +6,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/numeric_pair.h"
 #include "util/vector.h"
diff --git a/src/math/lp/matrix_def.h b/src/math/lp/matrix_def.h
index b9d5efb48..e3ac08f7e 100644
--- a/src/math/lp/matrix_def.h
+++ b/src/math/lp/matrix_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include <cmath>
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 4f7052ee5..1ed0956dc 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -6,7 +6,6 @@
   Lev Nachmanson (levnach)
 
   --*/
-// clang-format off
 
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_core.h"
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 2d7079c50..236f29bc0 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -6,7 +6,6 @@
   Lev Nachmanson (levnach)
 
   --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index e72af480b..e4087a407 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -4,7 +4,6 @@
   Author:
     Lev Nachmanson (levnach)
 --*/
-// clang-format off
 
 #pragma once
 #include <initializer_list>
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index ae73490f8..c43b723ef 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -4,7 +4,6 @@
   Author:
    Lev Nachmanson (levnach)
   --*/
-// clang-format off
 #include "util/lbool.h"
 #include "math/lp/nex_creator.h"
 #include <map>
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 4e147e373..9bce46395 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -5,7 +5,6 @@
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #pragma once
 #include <map>
 #include <set>
diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 99638d9d1..7124fd409 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -6,7 +6,6 @@
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_core.h"
diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h
index c913cfcfc..58fb0e92f 100644
--- a/src/math/lp/nla_basics_lemmas.h
+++ b/src/math/lp/nla_basics_lemmas.h
@@ -6,7 +6,6 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
-// clang-format off
 #pragma once
 #include "math/lp/monic.h"    
 #include "math/lp/factorization.h"    
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index d9f9b2bfc..45898c613 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -6,7 +6,6 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #include "math/lp/nla_common.h"
 #include "math/lp/nla_core.h"
 
diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h
index dc393af95..1302c3909 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -6,7 +6,6 @@
    Nikolaj Bjorner (nbjorner)
 
   --*/
-// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/nla_defs.h"
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 0931e005f..3c1f9da57 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -10,7 +10,6 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index e178fbf75..938bcbe83 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -10,7 +10,6 @@
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 #include "math/lp/lp_types.h"
diff --git a/src/math/lp/nla_defs.h b/src/math/lp/nla_defs.h
index 23be7bb72..df9158b42 100644
--- a/src/math/lp/nla_defs.h
+++ b/src/math/lp/nla_defs.h
@@ -8,7 +8,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #include "math/lp/lp_types.h"
 #include "math/lp/column_info.h"
diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp
index fd83de32c..cbb30d9d9 100644
--- a/src/math/lp/nla_divisions.cpp
+++ b/src/math/lp/nla_divisions.cpp
@@ -14,7 +14,6 @@ Description:
   Check divisions
 
 --*/
-// clang-format off
 #include "math/lp/nla_core.h"
 
 namespace nla {
diff --git a/src/math/lp/nla_divisions.h b/src/math/lp/nla_divisions.h
index e07cf3aed..80bf5be4e 100644
--- a/src/math/lp/nla_divisions.h
+++ b/src/math/lp/nla_divisions.h
@@ -13,7 +13,6 @@ Description:
   Check division constraints.
   
 --*/
-// clang-format off
 
 #include "math/lp/nla_types.h"
 
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 9cdb19fbf..974c48d14 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -10,7 +10,6 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 12f8609d7..902ad3a46 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -6,7 +6,6 @@
   Lev Nachmanson (levnach)
 
   --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/nla_common.h"
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 1806051ae..0545e9933 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -6,7 +6,6 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
-// clang-format off
 #pragma once
 #include "util/dependency.h"
 #include "util/region.h"
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index 2694a7ef8..cc9241446 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -5,7 +5,6 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_core.h"
 namespace nla {
diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h
index 2828e601c..d13f588e8 100644
--- a/src/math/lp/nla_monotone_lemmas.h
+++ b/src/math/lp/nla_monotone_lemmas.h
@@ -5,7 +5,6 @@
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #pragma once
 namespace nla {
 class core;
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 9b4b0e187..94ddc4d9b 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -5,7 +5,6 @@
     Nikolaj Bjorner (nbjorner)
     Lev Nachmanson (levnach)
   --*/
-// clang-format off
 
 #include "math/lp/nla_order_lemmas.h"
 #include "math/lp/nla_core.h"
diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h
index 025e4b783..c6961bc52 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -6,7 +6,6 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
-// clang-format off
 #pragma once
 #include "math/lp/factorization.h"
 #include "math/lp/nla_common.h"
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index bbf50e9a7..f389aad93 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -74,7 +74,6 @@ am().set(yval, am_value(y));
 am().set(rval, am_value(r));
 
 --*/
-// clang-format off
 #include "math/lp/nla_core.h"
 
 namespace nla {
diff --git a/src/math/lp/nla_powers.h b/src/math/lp/nla_powers.h
index f76460e1c..f74417ae3 100644
--- a/src/math/lp/nla_powers.h
+++ b/src/math/lp/nla_powers.h
@@ -13,7 +13,6 @@ Description:
   Refines bounds on powers.
   
 --*/
-// clang-format off
 
 #include "math/lp/nla_types.h"
 
diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h
index 6eb2ea1c3..ec11ea5b2 100644
--- a/src/math/lp/nla_settings.h
+++ b/src/math/lp/nla_settings.h
@@ -6,7 +6,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 
 #pragma once
 namespace nla {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index ada438edc..bd0f1953c 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -5,7 +5,6 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #include "math/lp/nla_solver.h"
 #include <map>
 #include "math/lp/monic.h"
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 8da4815aa..d04ff8e51 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -6,7 +6,6 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
-// clang-format off
 #pragma once
 #include "util/vector.h"
 #include "math/lp/lp_settings.h"
diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp
index c2081281e..4ba9eeccc 100644
--- a/src/math/lp/nla_tangent_lemmas.cpp
+++ b/src/math/lp/nla_tangent_lemmas.cpp
@@ -6,7 +6,6 @@
     Nikolaj Bjorner (nbjorner)
 
   --*/
-// clang-format off
 #include "math/lp/nla_tangent_lemmas.h"
 #include "math/lp/nla_core.h"
 
diff --git a/src/math/lp/nla_tangent_lemmas.h b/src/math/lp/nla_tangent_lemmas.h
index d3d71590d..1895b3fcb 100644
--- a/src/math/lp/nla_tangent_lemmas.h
+++ b/src/math/lp/nla_tangent_lemmas.h
@@ -5,7 +5,6 @@
     Lev Nachmanson (levnach)
     Nikolaj Bjorner (nbjorner)
   --*/
-// clang-format off
 #pragma once
 #include "util/rational.h"
 #include "math/lp/factorization.h"
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 1efc98860..8169266cc 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -13,7 +13,6 @@ Description:
   Types used for nla solver.
   
 --*/
-// clang-format off
 
 #pragma once
 
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index a59057288..251274006 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 #pragma once
 #define lp_for_z3
 #include <string>
diff --git a/src/math/lp/permutation_matrix.cpp b/src/math/lp/permutation_matrix.cpp
index 166330c6f..be4b7335c 100644
--- a/src/math/lp/permutation_matrix.cpp
+++ b/src/math/lp/permutation_matrix.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include "math/lp/permutation_matrix_def.h"
diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h
index b31d3cdec..a3fff4f7f 100644
--- a/src/math/lp/permutation_matrix.h
+++ b/src/math/lp/permutation_matrix.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <algorithm>
diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h
index e1bd8c4a8..c86fef4f4 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "util/vector.h"
diff --git a/src/math/lp/random_updater.cpp b/src/math/lp/random_updater.cpp
index 6535c840f..a88df76e5 100644
--- a/src/math/lp/random_updater.cpp
+++ b/src/math/lp/random_updater.cpp
@@ -17,6 +17,5 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include "math/lp/random_updater_def.h"
 
diff --git a/src/math/lp/random_updater.h b/src/math/lp/random_updater.h
index c90b1e6f2..d5cd4928c 100644
--- a/src/math/lp/random_updater.h
+++ b/src/math/lp/random_updater.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include <set>
diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h
index c31211e2c..7d167a4a0 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "math/lp/random_updater.h"
diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
index 8b7dd4812..ecd61eb10 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp
index c871ddc87..a46b5abc0 100644
--- a/src/math/lp/static_matrix.cpp
+++ b/src/math/lp/static_matrix.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include <set>
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 2e25b5b9a..ffbd48021 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -6,7 +6,6 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index c7fcc6d88..0370ee899 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 
 #include "util/vector.h"
diff --git a/src/math/lp/test_bound_analyzer.h b/src/math/lp/test_bound_analyzer.h
index 438deffda..1ca99d637 100644
--- a/src/math/lp/test_bound_analyzer.h
+++ b/src/math/lp/test_bound_analyzer.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #if 0
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/u_set.h b/src/math/lp/u_set.h
index 54778669d..ce59dccb7 100644
--- a/src/math/lp/u_set.h
+++ b/src/math/lp/u_set.h
@@ -18,7 +18,6 @@ Revision History:
 TBD use indexed_uint_set from src/util/uint_set.h, 
 
 --*/
-// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <ostream>
diff --git a/src/math/lp/ul_pair.h b/src/math/lp/ul_pair.h
index 95af719e0..abfb4483b 100644
--- a/src/math/lp/ul_pair.h
+++ b/src/math/lp/ul_pair.h
@@ -17,7 +17,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 
 #pragma once
 #include "util/vector.h"
diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h
index 88676715d..998779dc6 100644
--- a/src/math/lp/var_eqs.h
+++ b/src/math/lp/var_eqs.h
@@ -17,7 +17,6 @@
 
 
   --*/
-// clang-format off
 
 #pragma once
 #include "util/union_find.h"
diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h
index cea5ae2b6..49767274d 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -16,7 +16,6 @@ Revision History:
 
 
 --*/
-// clang-format off
 #pragma once
 #include "math/lp/lp_types.h"
 namespace lp  {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b21424e65..0c182dce5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3220,6 +3220,7 @@ public:
 
     lbool make_feasible() {
         TRACE("pcs",  tout << lp().constraints(););
+        TRACE("arith_verbose", tout << "before calling lp().find_feasible_solution()\n"; display(tout););
         auto status = lp().find_feasible_solution();
         TRACE("arith_verbose", display(tout););
         if (lp().is_feasible())