diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 464b3544c..edf22b76c 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -102,10 +102,8 @@ namespace smt {
         numeral new_range;
         numeral small_range_thresold(1024);
         unsigned n = 0;
-        typename vector<row>::const_iterator it  = m_rows.begin();
-        typename vector<row>::const_iterator end = m_rows.end();
-        for (; it != end; ++it) {
-            theory_var v = it->get_base_var();
+        for (row const& row : m_rows) {
+            theory_var v = row.get_base_var();
             if (v == null_theory_var)
                 continue;
             if (!is_base(v))
@@ -120,26 +118,19 @@ namespace smt {
             numeral const & u = upper_bound(v).get_rational();
             new_range  = u;
             new_range -= l;
-            if (new_range > small_range_thresold) 
-                continue;
-            if (result == null_theory_var) {
+            if (new_range > small_range_thresold) {
+                //
+            }
+            else if (result == null_theory_var || new_range < range) {
                 result = v;
                 range  = new_range;
                 n      = 1;
-                continue;
             }
-            if (new_range < range) {
-                n      = 1;
-                result = v;
-                range  = new_range;
-                continue;
-            }
-            if (new_range == range) {
+            else if (new_range == range) {
                 n++;
                 if (m_random() % n == 0) {
                     result = v;
                     range  = new_range;
-                    continue;
                 }
             }
         }
@@ -166,25 +157,41 @@ namespace smt {
         
 #define SELECT_VAR(VAR) if (r == null_theory_var) { n = 1; r = VAR; } else { n++; SASSERT(n >= 2); if (m_random() % n == 0) r = VAR; }
 
-        typename vector<row>::const_iterator it  = m_rows.begin();
-        typename vector<row>::const_iterator end = m_rows.end();
-        for (; it != end; ++it) {
-            theory_var v = it->get_base_var();
-            if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
-                SELECT_VAR(v);
+        numeral small_value(1024);
+        if (r == null_theory_var) {
+            for (auto const& row : m_rows) {
+                theory_var v = row.get_base_var();
+                if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
+                    if (abs(get_value(v)) < small_value) {
+                        SELECT_VAR(v);
+                    }
+                    else if (upper(v) && small_value > upper_bound(v) - get_value(v)) {
+                        SELECT_VAR(v);
+                    }
+                    else if (lower(v) && small_value > get_value(v) - lower_bound(v)) {
+                        SELECT_VAR(v);
+                    }
+                }
             }
         }
+
         if (r == null_theory_var) {
-            it  = m_rows.begin();
-            for (; it != end; ++it) {
-                theory_var v = it->get_base_var();
+            for (auto const& row : m_rows) {
+                theory_var v = row.get_base_var();
+                if (v != null_theory_var && is_base(v) && is_int(v) && !get_value(v).is_int()) {
+                    SELECT_VAR(v);
+                }
+            }
+        }
+
+        if (r == null_theory_var) {
+            for (auto const& row : m_rows) {
+                theory_var v = row.get_base_var();
                 if (v != null_theory_var && is_quasi_base(v) && is_int(v) && !get_value(v).is_int()) {
                     quasi_base_row2base_row(get_var_row(v));
                     SELECT_VAR(v);
                 }
             }
-            if (r == null_theory_var)
-                return null_theory_var;
         }
         CASSERT("arith", wf_rows());
         CASSERT("arith", wf_columns());