clean up and add clang-format off

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/gomory.cpp

@@ -17,6 +17,7 @@
 
 
   --*/
+// clang-format off
 #include "math/lp/gomory.h"
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"

src/math/lp/gomory.h

@@ -15,6 +15,7 @@ Author:
 
 Revision History:
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/lar_term.h"
 #include "math/lp/lia_move.h"

src/math/lp/int_branch.cpp

@@ -15,7 +15,7 @@
 
   Revision History:
   --*/
-
+// clang-format off
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/int_branch.h"
@@ -63,7 +63,7 @@ int int_branch::find_inf_int_base_column() {
     mpq small_value(1024);
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-    unsigned prev_usage = 0; // to quiet down the compile
+    unsigned prev_usage = 0; // to quiet down the compiler
     unsigned k = 0;
     unsigned usage;
     unsigned j;

src/math/lp/int_solver.cpp

@@ -878,9 +878,6 @@ int int_solver::select_int_infeasible_var() {
     enum state { small_box, is_small_value,  any_value, not_found };
     state st = not_found;
 
-    // 1. small box
-    // 2. small value
-    // 3. any value
     for (unsigned j : lra.r_basis()) {
         if (!column_is_int_inf(j))
             continue;

src/smt/theory_arith_int.h

@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/numeral_buffer.h"