diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 2ecbc49ac..babb10d72 100644
--- a/src/math/lp/gomory.cpp
+++ b/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"
diff --git a/src/math/lp/gomory.h b/src/math/lp/gomory.h
index 68e42feb9..acca900df 100644
--- a/src/math/lp/gomory.h
+++ b/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"
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index da34f77fd..47a9ddcbe 100644
--- a/src/math/lp/int_branch.cpp
+++ b/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;
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index af4488162..1c13ec25d 100644
--- a/src/math/lp/int_solver.cpp
+++ b/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;
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index c9bc9f31a..e89b81674 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+// clang-format off
 #pragma once
 
 #include "util/numeral_buffer.h"