diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index a283497c4..3976a0d3c 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -50,7 +50,7 @@ lia_move int_branch::create_branch_on_column(int j) {
     return lia_move::branch;        
 }
 
-    
+
     
 int int_branch::find_inf_int_base_column() {
     int result = -1;
@@ -59,41 +59,48 @@ int int_branch::find_inf_int_base_column() {
     mpq small_range_thresold(1024);
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
-    bool small = false;
     unsigned prev_usage;
-    for (unsigned j : lra.r_basis()) {
-        SASSERT(!lia.column_is_int_inf(j) || !lia.is_fixed(j));
+    unsigned k = 0;
+    unsigned usage;
+    unsigned j;
+    // this loop looks for a column with the most usages, but breaks when
+    // a column with a small span of bounds is found
+    for (; k < lra.r_basis().size(); k++) {
+        j = lra.r_basis()[k];
         if (!lia.column_is_int_inf(j))
             continue;
-        bool boxed = lia.is_boxed(j);
-        unsigned usage =  2 * lra.usage_in_terms(j);
-        if (small) {
-            if (!boxed)
-                continue;
-            new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage);
-            if (new_range <= small_range_thresold) {
-                if (new_range < range) {
-                    n = 1;
-                    result = j;
-                    range = new_range;
-                } else if (new_range == range && lia.random() % (++n) == 0) {
-                    result = j;                    
-                }
-            }
-        } else if (boxed && (
-                   (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(usage))
-                   <= small_range_thresold)) {
-            small = true;
+        usage = lra.usage_in_terms(j);
+        if (lia.is_boxed(j) &&  (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
             result = j;
+            k++;            
             n = 1;
-        } else if (result == -1 || prev_usage < usage) {
+            break;
+        }
+        if (n == 0 || usage > prev_usage) {
             result = j;
             prev_usage = usage;
-            n      = 1;
-        } else if (prev_usage == usage && lia.random() % (++n) == 0) {
+            n = 1;
+        } else if (usage == prev_usage && (lia.random() % (++n) == 0)) {
             result = j;
         }
     }
+    SASSERT(k == lra.r_basis().size() || n == 1);
+    // this loop looks for boxed columns with a small span
+    for (; k < lra.r_basis().size(); k++) {
+        j = lra.r_basis()[k];
+        usage = lra.usage_in_terms(j);
+        if (!lia.column_is_int_inf(j) || !lia.is_boxed(j))
+            continue;
+        SASSERT(!lia.is_fixed(j));
+        new_range  = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage);
+        if (new_range < range) {
+            n = 1;
+            result = j;
+            range = new_range;
+        } else if (new_range == range && (lia.random() % (++n) == 0)) {
+            result = j;                    
+        }
+    }
     return result;    
 }