diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 62516c91b..f658553ea 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -450,28 +450,24 @@ void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const
     auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
     auto delta = new_val - x;
     x = new_val;
+    TRACE("int_solver", tout << "x[" << j << "] = " << x << "\n";);
     m_lar_solver->change_basic_columns_dependend_on_a_given_nb_column(j, delta);
 }
 
-void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
+void int_solver::patch_nbasic_column(unsigned j) {
     auto & lcs = m_lar_solver->m_mpq_lar_core_solver; 
     impq & val = lcs.m_r_x[j];
-    bool val_is_int = val.is_int();
-    if (patch_only_int_vals && !val_is_int)
-        return;
-        
     bool inf_l, inf_u;
     impq l, u;
     mpq m;
-    if (!get_freedom_interval_for_column(j, val_is_int, inf_l, l, inf_u, u, m)) {
+    if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m)) {
         return;
     }
     bool m_is_one = m.is_one();
-    if (m.is_one() && val_is_int) {
-        return;
-    }
+    bool val_is_int = value_is_int(j);
+
     // check whether value of j is already a multiple of m.
-    if (val_is_int && (val.x / m).is_int()) {
+    if (val_is_int && (m_is_one || (val.x / m).is_int())) {
         return;
     }
     TRACE("patch_int",
@@ -506,7 +502,7 @@ lia_move int_solver::patch_nbasic_columns() {
     settings().stats().m_patches++;
     lp_assert(is_feasible());
     for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_nbasis) {
-        patch_nbasic_column(j, settings().m_int_patch_only_integer_values);
+        patch_nbasic_column(j);
     }
     lp_assert(is_feasible());
     if (!has_inf_int()) {
@@ -734,11 +730,12 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
     }
 }
 
-bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
+bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
     auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
     if (lcs.m_r_heading[j] >= 0) // the basic var 
         return false;
 
+    TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);
     impq const & xj = get_value(j);
     
     inf_l = true;
@@ -753,7 +750,6 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bo
         set_upper(u, inf_u, upper_bound(j) - xj);
     }
 
-    mpq a; // the coefficient in the column
     unsigned row_index;
     lp_assert(settings().use_tableau());
     const auto & A = m_lar_solver->A_r();
@@ -762,11 +758,11 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bo
         row_index = c.var();
         const mpq & a = c.coeff();        
         unsigned i = lcs.m_r_basis[row_index];
-        if (column_is_int(i) && column_is_int(j) && !a.is_int())
+        TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";); 
+        if (!a.is_int())
             m = lcm(m, denominator(a));
     }
-    if (val_is_int && m.is_one())
-        return false;
+    TRACE("random_update", tout <<  "m = " << m << "\n";);
     
     for (const auto &c : A.column(j)) {
         if (!inf_l && !inf_u && l >= u) break;                
@@ -845,8 +841,9 @@ const impq & int_solver::get_value(unsigned j) const {
     return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
 }
 
-void int_solver::display_column(std::ostream & out, unsigned j) const {
+std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
     m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
+    return out;
 }
 
 bool int_solver::column_is_int_inf(unsigned j) const {
@@ -928,6 +925,8 @@ unsigned int_solver::random() {
     return m_lar_solver->get_core_solver().settings().random_next();
 }
 
+
+// at this point the 
 bool int_solver::shift_var(unsigned j, unsigned range) {
     if (is_fixed(j) || is_base(j))
         return false;
@@ -935,55 +934,49 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     bool inf_l, inf_u;
     impq l, u;
     mpq m;
-    get_freedom_interval_for_column(j, false, inf_l, l, inf_u, u, m);
+    get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
+    const impq & x = get_value(j);
+    // x, the value of j column, might be shifted on a multiple of m
     if (inf_l && inf_u) {
-        impq new_val = impq(random() % (range + 1));
+        impq new_val = m * impq(random() % (range + 1)) + x;
         set_value_for_nbasic_column_ignore_old_values(j, new_val);
         return true;
     }
     if (column_is_int(j)) {
         if (!inf_l) {
             l = impq(ceil(l));
-            if (!m.is_one())
-                l = impq(m*ceil(l/m));
         }
         if (!inf_u) {
             u = impq(floor(u));
-            if (!m.is_one())
-                u = impq(m*floor(u/m));
         }
     }
     if (!inf_l && !inf_u && l >= u)
         return false;
+
     if (inf_u) {
         SASSERT(!inf_l);
-        impq delta   = impq(random() % (range + 1));
-        impq new_val = l + m*delta;
+        impq new_val = x + m * impq(random() % (range + 1));
         set_value_for_nbasic_column_ignore_old_values(j, new_val);
         return true;
     }
+
     if (inf_l) {
         SASSERT(!inf_u);
-        impq delta   = impq(random() % (range + 1));
-        impq new_val = u - m*delta;
-        set_value_for_nbasic_column_ignore_old_values(j, new_val);
-        return true;
-    }
-    if (!column_is_int(j)) {
-        SASSERT(!inf_l && !inf_u);
-        mpq delta       = mpq(random() % (range + 1));
-        impq new_val = l + ((delta * (u - l)) / mpq(range)); 
-        set_value_for_nbasic_column_ignore_old_values(j, new_val);
-        return true;
-    }
-    else {
-        mpq r = (u.x - l.x) / m;
-        if (r < mpq(range))
-            range = static_cast<unsigned>(r.get_uint64());
-        impq new_val = l + m * (impq(random() % (range + 1)));
+        impq new_val = x - m * impq(random() % (range + 1));
         set_value_for_nbasic_column_ignore_old_values(j, new_val);
         return true;
     }
+
+    SASSERT(!inf_l && !inf_u);
+    mpq r = floor((u.x - l.x) / m);
+    if (r < mpq(range)) range = static_cast<unsigned>(r.get_uint64());
+    // the interval contains at least range multiples of m.
+    // the number of multiples to the left of the value of j is floor((get_value(j) - l.x)/m)
+    // shift either left or right of the current value by available multiples.
+    impq shift = impq(random() % (range + 1)) - impq(floor(x.x - l.x) / m);
+    impq new_val = x + m * shift;
+    SASSERT(l <= new_val && new_val <= u);
+    set_value_for_nbasic_column_ignore_old_values(j, new_val);    return true;
 }
 
 bool int_solver::non_basic_columns_are_at_bounds() const {
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index df60afee3..955371e1a 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -88,7 +88,7 @@ private:
     void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
     void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
     lia_move patch_nbasic_columns();
-    bool get_freedom_interval_for_column(unsigned j, bool val_is_int, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
+    bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
 private:
     bool is_boxed(unsigned j) const;
     bool is_fixed(unsigned j) const;
@@ -121,7 +121,7 @@ private:
     unsigned row_of_basic_column(unsigned j) const;
 
 public:
-    void display_column(std::ostream & out, unsigned j) const;
+    std::ostream& display_column(std::ostream & out, unsigned j) const;
     constraint_index column_upper_bound_constraint(unsigned j) const;
     constraint_index column_lower_bound_constraint(unsigned j) const;
     bool current_solution_is_inf_on_cut() const;
@@ -152,6 +152,6 @@ public:
     void try_add_term_to_A_for_hnf(unsigned term_index);
     bool hnf_has_var_with_non_integral_value() const;
     bool hnf_cutter_is_full() const;
-    void patch_nbasic_column(unsigned j, bool patch_only_int_vals);
+    void patch_nbasic_column(unsigned j);
   };
 }
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6232183ed..9505ff2a0 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -612,7 +612,7 @@ lp_status lar_solver::maximize_term(unsigned j_or_term,
                 return lp_status::FEASIBLE; // it should not happen
             }
         }
-        m_int_solver->patch_nbasic_column(j, false);
+        m_int_solver->patch_nbasic_column(j);
         if (!column_value_is_integer(j)) {
             term_max = prev_value;
             m_mpq_lar_core_solver.m_r_x = backup;
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 456f082c7..a7d7e9b86 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -196,7 +196,6 @@ private:
 public:
     bool             m_int_run_gcd_test;
     bool             m_int_pivot_fixed_vars_from_basis;
-    bool             m_int_patch_only_integer_values;
     unsigned         limit_on_rows_for_hnf_cutter;
     unsigned         limit_on_columns_for_hnf_cutter;
     bool             m_enable_hnf;
@@ -268,7 +267,6 @@ public:
                     m_hnf_cut_period(4),
                     m_int_run_gcd_test(true),
                     m_int_pivot_fixed_vars_from_basis(false),
-                    m_int_patch_only_integer_values(true),
                     limit_on_rows_for_hnf_cutter(75),
                     limit_on_columns_for_hnf_cutter(150),
                     m_enable_hnf(true),
diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h
index fd8c2305a..b90175646 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -39,13 +39,6 @@ bool random_updater::shift_var(unsigned v) {
     return m_lar_solver.get_int_solver()->shift_var(v, m_range);
 }
 
-bool random_updater::random_shift_var(unsigned j) {
-    if (m_lar_solver.A_r().m_columns.size() >= 50) {
-        return false;
-    }
-
-    return shift_var(j);
-}
 
 void random_updater::update() {
     for (auto j : m_var_set) {
@@ -53,7 +46,7 @@ void random_updater::update() {
             break; // we are done
         }
         auto old_x = m_lar_solver.get_column_value(j);
-        if (random_shift_var(j)) {
+        if (shift_var(j)) {
             remove_value(old_x);
             add_value(m_lar_solver.get_column_value(j));
         }