diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 45654310f..0622f03ff 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1451,6 +1451,11 @@ namespace smt {
             normalize_gain(min_gain.get_rational(), max_gain);
         }
 
+        if (is_int(x_i) && !max_gain.is_rational()) {
+            max_gain = inf_numeral(floor(max_gain));
+            normalize_gain(min_gain.get_rational(), max_gain);
+        }
+
         if (!max_inc.is_minus_one()) {
             if (is_int(x_i)) {
                 TRACE("opt",
@@ -1597,6 +1602,7 @@ namespace smt {
 
             TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
                   tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
+
             
             if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) {
                 has_shared = false;