diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index fc0e2be4a..51f804682 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2435,7 +2435,7 @@ void lar_solver::pivot_column_tableau(unsigned j, unsigned row_index) {
     m_mpq_lar_core_solver.m_r_solver.pivot_column_tableau(j, row_index);
     m_mpq_lar_core_solver.m_r_solver.change_basis(j, r_basis()[row_index]);
 }
-
+#if 0
 bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool (lpvar)>& blocker, const std::function<void (lpvar)>& report_change) {
     if (is_base(j)) {
         TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
@@ -2470,7 +2470,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
 
     return true;
 }
-
+#endif
 } // namespace lp
 
 
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index f563d0594..bf6efb1f5 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -306,7 +306,41 @@ public:
     bool column_corresponds_to_term(unsigned) const;
     inline unsigned row_count() const { return A_r().row_count(); }
     bool var_is_registered(var_index vj) const;
-    bool try_to_patch(lpvar, const mpq&, const std::function<bool (lpvar)>& blocker,const std::function<void (lpvar)>& change_report);
+    template <typename Blocker, typename ChangeReport>
+    bool try_to_patch(lpvar j, const mpq& val, const std::function<bool (lpvar)>& blocker,const std::function<void (lpvar)>& change_report) {
+        if (is_base(j)) {
+            TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
+            remove_from_basis(j);
+        }
+
+        impq ival(val);
+        if (!inside_bounds(j, ival) || blocker(j))
+            return false;
+
+        impq delta = get_column_value(j) - ival;
+        for (const auto &c : A_r().column(j)) {
+            unsigned row_index = c.var();
+            const mpq & a = c.coeff();        
+            unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
+            impq rj_new_val = a * delta + get_column_value(rj);
+            if (column_is_int(rj) && !rj_new_val.is_int())
+                return false;
+            if (!inside_bounds(rj, rj_new_val) || blocker(rj))
+                return false;
+        }
+
+        set_column_value(j, ival);
+        change_report(j);
+        for (const auto &c : A_r().column(j)) {
+            unsigned row_index = c.var();
+            const mpq & a = c.coeff();        
+            unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
+            m_mpq_lar_core_solver.m_r_solver.add_delta_to_x(rj, a * delta);
+            change_report(rj);
+        }
+
+        return true;
+    }
     inline bool column_has_upper_bound(unsigned j) const {
         return m_mpq_lar_core_solver.m_r_solver.column_has_upper_bound(j);
     }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 89b07b9ba..1de52130d 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1308,7 +1308,8 @@ bool core::patch_blocker(lpvar u, const monic& m) const {
 bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
     auto blocker = [this, k, m](lpvar u) { return u != k && patch_blocker(u, m); };
     auto change_report = [this](lpvar u) { update_to_refine_of_var(u); };
-    return m_lar_solver.try_to_patch(k, v, blocker,  change_report);
+    return m_lar_solver.try_to_patch<std::function<bool(lpvar)>,
+                                     std::function<void(lpvar)>>(k, v, blocker,  change_report);
 }
 
 bool in_power(const svector<lpvar>& vs, unsigned l) {
@@ -1341,8 +1342,6 @@ void core::patch_monomial(lpvar j) {
         erase_from_to_refine(j);
         return;
     }
-    if (val(j).is_zero() || v.is_zero()) // a lemma will catch it
-        return;
 
     if (!var_breaks_correct_monic(j) && try_to_patch(j, v, m)) {
         SASSERT(to_refine_is_correct());        
@@ -1364,19 +1363,22 @@ void core::patch_monomial(lpvar j) {
     }
     // We have v != abc. Let us suppose we patch b. Then b should
     // be equal to v/ac = v/(abc/b) = b(v/abc)
-    rational r = val(j) / v;
-    SASSERT(m.is_sorted());
-    for (unsigned l = 0; l < m.size(); l++) {
-        lpvar k = m.vars()[l];
-        if (!in_power(m.vars(), l) &&
-            !var_is_int(k) && 
-            !var_breaks_correct_monic(k) &&
-            try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
-            SASSERT(mul_val(m) == var_val(m));
-            erase_from_to_refine(j);
-            break;
+    if (!v.is_zero()) {
+        rational r = val(j) / v;
+        SASSERT(m.is_sorted());
+    
+        for (unsigned l = 0; l < m.size(); l++) {
+            lpvar k = m.vars()[l];
+            if (!in_power(m.vars(), l) &&
+                !var_is_int(k) && 
+                !var_breaks_correct_monic(k) &&
+                try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
+                SASSERT(mul_val(m) == var_val(m));
+                erase_from_to_refine(j);
+                break;
+            }
         }
-    }                              
+    }
 }
 
 void core::patch_monomials() {