From 9be7bda69a06682c7e4f59004ce02a9e74a3fa3f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 29 Mar 2020 13:51:39 -0700
Subject: [PATCH] fix a bug in column patching

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp | 4 ++--
 src/math/lp/nla_core.cpp   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 5e782e58b..01f409cad 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2399,7 +2399,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, std::function<bool (lpvar
     if (!inside_bounds(j, ival))
         return false;
 
-    impq delta = ival - get_column_value(j);
+    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();        
@@ -2416,7 +2416,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, std::function<bool (lpvar
         unsigned row_index = c.var();
         const mpq & a = c.coeff();        
         unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
-        set_column_value(rj,a * delta + get_column_value(rj));
+        m_mpq_lar_core_solver.m_r_solver.add_delta_to_x(rj, a * delta);
         report_change(rj);
     }
     return true;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 5cad0056d..7c32270cb 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1357,7 +1357,7 @@ void core::update_to_refine_of_var(lpvar j) {
 
 
 
-void core::patch_real_var(lpvar j) {
+void core::patch_real_var(lpvar j) {    
     SASSERT(!var_is_int(j));
     rational v = mul_val(emons()[j]);
     if (val(j) == v)