diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 0008a0ee9..bfae22f21 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -19,6 +19,7 @@ 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 1dc0c60c7..c0b09e21f 100644
--- a/src/math/lp/column_info.h
+++ b/src/math/lp/column_info.h
@@ -17,6 +17,7 @@ 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 cef58ed21..ccd3cffad 100644
--- a/src/math/lp/column_namer.h
+++ b/src/math/lp/column_namer.h
@@ -18,6 +18,7 @@ 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 18bef8303..e1ce8fb1b 100644
--- a/src/math/lp/core_solver_pretty_printer.cpp
+++ b/src/math/lp/core_solver_pretty_printer.cpp
@@ -17,6 +17,7 @@ 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 5bf29d511..46e9ebf7e 100644
--- a/src/math/lp/core_solver_pretty_printer.h
+++ b/src/math/lp/core_solver_pretty_printer.h
@@ -17,6 +17,7 @@ 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 b8048b241..17f82af9c 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -17,6 +17,7 @@ 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 a39ef5ef9..9633e2dab 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #pragma once
 #include <functional>
 #include "math/lp/nex.h"
diff --git a/src/math/lp/dense_matrix.cpp b/src/math/lp/dense_matrix.cpp
index 25fc65a5d..cd8e019e6 100644
--- a/src/math/lp/dense_matrix.cpp
+++ b/src/math/lp/dense_matrix.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include "math/lp/lp_settings.h"
 #include "math/lp/dense_matrix_def.h"
 #ifdef Z3DEBUG
diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h
index fcc85cdd1..6b039a920 100644
--- a/src/math/lp/dense_matrix.h
+++ b/src/math/lp/dense_matrix.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #ifdef Z3DEBUG
 #include "util/vector.h"
diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h
index e850a9acd..986a2d20e 100644
--- a/src/math/lp/dense_matrix_def.h
+++ b/src/math/lp/dense_matrix_def.h
@@ -17,6 +17,7 @@ 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 bcdb81dd8..e5da7c702 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -18,6 +18,7 @@
   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 e4f4f4848..8f0f33175 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -18,6 +18,7 @@
     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 b7f721a30..67df7bab9 100644
--- a/src/math/lp/explanation.h
+++ b/src/math/lp/explanation.h
@@ -17,6 +17,7 @@ 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 b233894ad..aad52c58e 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -18,6 +18,7 @@
 
 
   --*/
+// 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 ace85a050..1406d5864 100644
--- a/src/math/lp/factorization_factory_imp.cpp
+++ b/src/math/lp/factorization_factory_imp.cpp
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 599039094..7c76299dc 100644
--- a/src/math/lp/factorization_factory_imp.h
+++ b/src/math/lp/factorization_factory_imp.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 a4f6693a2..0fc9c404b 100644
--- a/src/math/lp/general_matrix.h
+++ b/src/math/lp/general_matrix.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <functional>
 namespace lp {
diff --git a/src/math/lp/hnf.h b/src/math/lp/hnf.h
index 75a69393f..53b33b37a 100644
--- a/src/math/lp/hnf.h
+++ b/src/math/lp/hnf.h
@@ -26,6 +26,7 @@ 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 3c4ea10ab..e2fd85866 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -9,6 +9,7 @@ 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 b3530ea29..98f9770e8 100644
--- a/src/math/lp/hnf_cutter.h
+++ b/src/math/lp/hnf_cutter.h
@@ -14,6 +14,7 @@ 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 4d4ac4975..3b4cce827 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 2b6fc3cd8..ce630b0c2 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 9435edcdc..239103035 100644
--- a/src/math/lp/implied_bound.h
+++ b/src/math/lp/implied_bound.h
@@ -17,6 +17,7 @@ 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 0bb2829eb..f124eb05e 100644
--- a/src/math/lp/incremental_vector.h
+++ b/src/math/lp/incremental_vector.h
@@ -17,6 +17,7 @@ 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 92d8f2adf..aab13fc9c 100644
--- a/src/math/lp/indexed_value.h
+++ b/src/math/lp/indexed_value.h
@@ -17,6 +17,7 @@ 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 fe0892541..f5c34e1f9 100644
--- a/src/math/lp/indexed_vector.cpp
+++ b/src/math/lp/indexed_vector.cpp
@@ -17,6 +17,7 @@ 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 9f3119e9a..b5f5e6cb8 100644
--- a/src/math/lp/indexed_vector.h
+++ b/src/math/lp/indexed_vector.h
@@ -17,6 +17,7 @@ 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 034325088..c6f530d99 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"
diff --git a/src/math/lp/int_branch.h b/src/math/lp/int_branch.h
index 9601cb65e..6943bede5 100644
--- a/src/math/lp/int_branch.h
+++ b/src/math/lp/int_branch.h
@@ -15,6 +15,7 @@ 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 da724a543..787b82da7 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -15,6 +15,7 @@ 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 4addc096b..9ac6773ab 100644
--- a/src/math/lp/int_cube.h
+++ b/src/math/lp/int_cube.h
@@ -19,6 +19,7 @@ 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 4801cc436..e243783cc 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -45,6 +45,7 @@ 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 28ac2f7b3..b77179409 100644
--- a/src/math/lp/int_gcd_test.h
+++ b/src/math/lp/int_gcd_test.h
@@ -24,6 +24,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 #pragma once
 
 #include "math/lp/lia_move.h"
diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
index f8cffbe57..3bb6e7882 100644
--- a/src/math/lp/lar_constraints.h
+++ b/src/math/lp/lar_constraints.h
@@ -17,6 +17,7 @@ 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 09d01f4cc..bdb89f76b 100644
--- a/src/math/lp/lar_core_solver.cpp
+++ b/src/math/lp/lar_core_solver.cpp
@@ -17,6 +17,7 @@ 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 10cd53141..a67eb4d48 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -5,6 +5,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 #pragma once
 #include "util/vector.h"
 #include <string>
@@ -16,7 +17,7 @@ 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 942c87b3b..3f7866717 100644
--- a/src/math/lp/lar_core_solver_def.h
+++ b/src/math/lp/lar_core_solver_def.h
@@ -9,6 +9,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <string>
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 9c45fdb80..e9e26ffe6 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 fc73f949f..65262d5dd 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 ca61d7b7a..b1505dbc9 100644
--- a/src/math/lp/lia_move.h
+++ b/src/math/lp/lia_move.h
@@ -17,6 +17,7 @@ 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 2a4e5058d..9d0bd2476 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -7,6 +7,7 @@ Author:
     Nikolaj Bjorner (nbjorner)
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/inf_rational.h"
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
index 28f92d8e2..1859630e4 100644
--- a/src/math/lp/lp_core_solver_base.cpp
+++ b/src/math/lp/lp_core_solver_base.cpp
@@ -17,6 +17,7 @@ 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 f38587573..06e67cbf7 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include <set>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 319966091..756ff9af3 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -17,6 +17,7 @@ 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 efbfd27e1..0698c9962 100644
--- a/src/math/lp/lp_primal_core_solver.cpp
+++ b/src/math/lp/lp_primal_core_solver.cpp
@@ -17,6 +17,7 @@ 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 470405581..2a4a278a6 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -159,7 +159,7 @@ namespace lp {
     }
     return r;
   }
-    // clang-format on
+    // clang-format off
     int find_beneficial_entering_in_row_tableau_rows_bland_mode(int i, T &a_ent) {
         int j = -1;
         unsigned bj = this->m_basis[i];
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index e18a5ef05..909dfd086 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -17,6 +17,7 @@ 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 dbcced4ab..905bbba3c 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -17,6 +17,7 @@ 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 b72b837fd..723a4ba2d 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -17,6 +17,7 @@ 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 727bc3531..4e03007bb 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -17,6 +17,7 @@ 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 a19558949..12c53551f 100644
--- a/src/math/lp/lp_settings_def.h
+++ b/src/math/lp/lp_settings_def.h
@@ -17,6 +17,7 @@ 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 e4ee535aa..6f1f2e3d4 100644
--- a/src/math/lp/lp_types.h
+++ b/src/math/lp/lp_types.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include <sstream>
diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h
index 3c1383cb3..3a796c42b 100644
--- a/src/math/lp/lp_utils.h
+++ b/src/math/lp/lp_utils.h
@@ -17,6 +17,7 @@ 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 1ea2da263..1176a6358 100644
--- a/src/math/lp/matrix.cpp
+++ b/src/math/lp/matrix.cpp
@@ -17,6 +17,7 @@ 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 88a405614..306f43a57 100644
--- a/src/math/lp/matrix.h
+++ b/src/math/lp/matrix.h
@@ -6,6 +6,7 @@ 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 e3ac08f7e..b9d5efb48 100644
--- a/src/math/lp/matrix_def.h
+++ b/src/math/lp/matrix_def.h
@@ -17,6 +17,7 @@ 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 1ed0956dc..4f7052ee5 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -6,6 +6,7 @@
   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 236f29bc0..2d7079c50 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -6,6 +6,7 @@
   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 e4087a407..e72af480b 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -4,6 +4,7 @@
   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 c43b723ef..ae73490f8 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -4,6 +4,7 @@
   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 9bce46395..4e147e373 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -5,6 +5,7 @@
    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 7124fd409..99638d9d1 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -6,6 +6,7 @@
     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 58fb0e92f..c913cfcfc 100644
--- a/src/math/lp/nla_basics_lemmas.h
+++ b/src/math/lp/nla_basics_lemmas.h
@@ -6,6 +6,7 @@
     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 45898c613..d9f9b2bfc 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -6,6 +6,7 @@
     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 1302c3909..dc393af95 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -6,6 +6,7 @@
    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 3c1f9da57..0931e005f 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -10,6 +10,7 @@ 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 938bcbe83..e178fbf75 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -10,6 +10,7 @@
     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 df9158b42..23be7bb72 100644
--- a/src/math/lp/nla_defs.h
+++ b/src/math/lp/nla_defs.h
@@ -8,6 +8,7 @@
 
 
   --*/
+// 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 cbb30d9d9..fd83de32c 100644
--- a/src/math/lp/nla_divisions.cpp
+++ b/src/math/lp/nla_divisions.cpp
@@ -14,6 +14,7 @@ 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 80bf5be4e..e07cf3aed 100644
--- a/src/math/lp/nla_divisions.h
+++ b/src/math/lp/nla_divisions.h
@@ -13,6 +13,7 @@ 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 974c48d14..9cdb19fbf 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -10,6 +10,7 @@ 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 902ad3a46..12f8609d7 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -6,6 +6,7 @@
   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 0545e9933..1806051ae 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -6,6 +6,7 @@
     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 cc9241446..2694a7ef8 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -5,6 +5,7 @@
     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 d13f588e8..2828e601c 100644
--- a/src/math/lp/nla_monotone_lemmas.h
+++ b/src/math/lp/nla_monotone_lemmas.h
@@ -5,6 +5,7 @@
    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 94ddc4d9b..9b4b0e187 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -5,6 +5,7 @@
     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 c6961bc52..025e4b783 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -6,6 +6,7 @@
     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 f389aad93..bbf50e9a7 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -74,6 +74,7 @@ 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 f74417ae3..f76460e1c 100644
--- a/src/math/lp/nla_powers.h
+++ b/src/math/lp/nla_powers.h
@@ -13,6 +13,7 @@ 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 ec11ea5b2..6eb2ea1c3 100644
--- a/src/math/lp/nla_settings.h
+++ b/src/math/lp/nla_settings.h
@@ -6,6 +6,7 @@ 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 bd0f1953c..ada438edc 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -5,6 +5,7 @@
     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 d04ff8e51..8da4815aa 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -6,6 +6,7 @@ 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 4ba9eeccc..c2081281e 100644
--- a/src/math/lp/nla_tangent_lemmas.cpp
+++ b/src/math/lp/nla_tangent_lemmas.cpp
@@ -6,6 +6,7 @@
     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 1895b3fcb..d3d71590d 100644
--- a/src/math/lp/nla_tangent_lemmas.h
+++ b/src/math/lp/nla_tangent_lemmas.h
@@ -5,6 +5,7 @@
     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 8169266cc..1efc98860 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -13,6 +13,7 @@ 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 251274006..a59057288 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 be4b7335c..166330c6f 100644
--- a/src/math/lp/permutation_matrix.cpp
+++ b/src/math/lp/permutation_matrix.cpp
@@ -17,6 +17,7 @@ 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 a3fff4f7f..b31d3cdec 100644
--- a/src/math/lp/permutation_matrix.h
+++ b/src/math/lp/permutation_matrix.h
@@ -17,6 +17,7 @@ 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 c86fef4f4..e1bd8c4a8 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -17,6 +17,7 @@ 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 a88df76e5..6535c840f 100644
--- a/src/math/lp/random_updater.cpp
+++ b/src/math/lp/random_updater.cpp
@@ -17,5 +17,6 @@ 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 d5cd4928c..c90b1e6f2 100644
--- a/src/math/lp/random_updater.h
+++ b/src/math/lp/random_updater.h
@@ -17,6 +17,7 @@ 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 7d167a4a0..c31211e2c 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -17,6 +17,7 @@ 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 ecd61eb10..8b7dd4812 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -17,6 +17,7 @@ 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 efb6e07cf..c871ddc87 100644
--- a/src/math/lp/static_matrix.cpp
+++ b/src/math/lp/static_matrix.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #include <memory>
 #include "util/vector.h"
 #include <set>
@@ -29,7 +30,6 @@ namespace lp {
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();
 template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;
-template void static_matrix<mpq, mpq>::add_columns_at_the_end(unsigned int);
 template bool static_matrix<mpq, mpq>::is_correct() const;
 
 template mpq static_matrix<mpq, mpq>::get_balance() const;
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index f79ff36ac..2e25b5b9a 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -6,6 +6,7 @@ Author:
     Lev Nachmanson (levnach)
 
 --*/
+// clang-format off
 
 #pragma once
 #include "util/vector.h"
@@ -126,7 +127,6 @@ public:
 
     unsigned lowest_row_in_column(unsigned col);
 
-    void add_columns_at_the_end(unsigned delta);
     void add_new_element(unsigned i, unsigned j, const T & v);
 
     void add_row() {m_rows.push_back(row_strip<T>());}
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index 76c1dec54..c7fcc6d88 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/vector.h"
@@ -124,11 +125,6 @@ template <typename T, typename X> unsigned static_matrix<T, X>::lowest_row_in_co
     return ret;
 }
 
-template <typename T, typename X> void static_matrix<T, X>::add_columns_at_the_end(unsigned delta) {
-    for (unsigned i = 0; i < delta; i++)
-        add_column();
-}
-
 template <typename T, typename X> void static_matrix<T, X>::forget_last_columns(unsigned how_many_to_forget) {
     lp_assert(m_columns.size() >= how_many_to_forget);
     unsigned j = column_count() - 1;
diff --git a/src/math/lp/test_bound_analyzer.h b/src/math/lp/test_bound_analyzer.h
index 1ca99d637..438deffda 100644
--- a/src/math/lp/test_bound_analyzer.h
+++ b/src/math/lp/test_bound_analyzer.h
@@ -17,6 +17,7 @@ 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 ce59dccb7..54778669d 100644
--- a/src/math/lp/u_set.h
+++ b/src/math/lp/u_set.h
@@ -18,6 +18,7 @@ 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 abfb4483b..95af719e0 100644
--- a/src/math/lp/ul_pair.h
+++ b/src/math/lp/ul_pair.h
@@ -17,6 +17,7 @@ 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 998779dc6..88676715d 100644
--- a/src/math/lp/var_eqs.h
+++ b/src/math/lp/var_eqs.h
@@ -17,6 +17,7 @@
 
 
   --*/
+// 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 49767274d..cea5ae2b6 100644
--- a/src/math/lp/var_register.h
+++ b/src/math/lp/var_register.h
@@ -16,6 +16,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/lp_types.h"
 namespace lp  {
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 159758c80..0a4c1869b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 #pragma once
-
+// clang-format off
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt2_pp.h"