diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 0436c2ebf..d943c22a5 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -45,10 +45,8 @@ int int_solver::find_gomory_cut_column() {
     mpq min_range;
 
     // Prefer smaller row size
-#if 0
     // Prefer boxed to non-boxed
     // Prefer smaller ranges
-#endif
 
     for (unsigned j : m_lar_solver->r_basis()) {
         if (!column_is_int_inf(j))
@@ -56,7 +54,7 @@ int int_solver::find_gomory_cut_column() {
         const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
         if (!is_gomory_cut_target(row)) 
             continue;
-#if 1
+
         if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
             lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
             auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
@@ -76,7 +74,6 @@ int int_solver::find_gomory_cut_column() {
                 continue;
             }
         }
-#endif
         if (min_row_size == UINT_MAX || (4*row.size() < 5*min_row_size && random() % (++n) == 0)) {
             result = j;
             n = 1;
@@ -191,12 +188,8 @@ lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row
 
 lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
     const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
-
-    SASSERT(m_lar_solver->row_is_correct(row_of_basic_column(j)));
-    
-    if (!is_gomory_cut_target(row)) 
-        return create_branch_on_column(j);
-
+    SASSERT(m_lar_solver->row_is_correct(row_of_basic_column(j)));    
+    SASSERT(is_gomory_cut_target(row));
     m_upper = true;
     return mk_gomory_cut(j, row);
 }
@@ -353,13 +346,12 @@ lia_move int_solver::gomory_cut() {
         lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
     }
         
-//    int j = find_inf_int_base_column();
     int j = find_gomory_cut_column(); 
-    if (j == -1) {
-        j = find_inf_int_nbasis_column();
-        return j == -1? lia_move::sat : create_branch_on_column(j);
+    if (j != -1) {
+        return proceed_with_gomory_cut(j);
     }
-    return proceed_with_gomory_cut(j);
+    j = find_inf_int_nbasis_column();
+    return j == -1? lia_move::sat : create_branch_on_column(j);    
 }
 
 void int_solver::try_add_term_to_A_for_hnf(unsigned i) {