From 6a5579341d84f63979a11caa7718bca0ba1189ec Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 26 May 2020 17:27:55 -0700
Subject: [PATCH] add restore_patched_values

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

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index baab8c18e..527ad980f 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -266,10 +266,10 @@ class lar_solver : public column_namer {
     void register_normalized_term(const lar_term&, lpvar);
     void deregister_normalized_term(const lar_term&);
     bool inside_bounds(lpvar, const impq&) const;
+public:
     inline void set_column_value(unsigned j, const impq& v) {
         m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
     }
-public:
     inline void set_column_value_test(unsigned j, const impq& v) {
         set_column_value(j, v);
     }
@@ -306,7 +306,9 @@ 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;
-
+    inline void remove_column_from_inf_set(unsigned j) {
+        m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
+    }
     template <typename CallBeforeChange, typename ChangeReport>
     void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j,
                                                                     const numeric_pair<mpq> & delta,
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 7f9920ad0..bd882e161 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1381,6 +1381,13 @@ void core::patch_monomial(lpvar j) {
     }
 }
 
+void core::restore_patched_values() {
+    for (const auto & p : m_changes_of_patch) {
+        m_lar_solver.set_column_value(p.m_key, lp::impq(p.m_value));
+        m_lar_solver.remove_column_from_inf_set(p.m_key);
+    }
+}
+
 void core::patch_monomials() {
     m_changes_of_patch.reset();
     auto to_refine = m_to_refine.index();
@@ -1393,6 +1400,9 @@ void core::patch_monomials() {
         if (m_to_refine.size() == 0)
             break;
     }
+    if (m_to_refine.size()) {
+        restore_patched_values();
+    }
     NOT_IMPLEMENTED_YET();
     /*
       If the tableau is not feasible we need to fix all non-linear
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 32e9e5668..430348e89 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -480,6 +480,8 @@ public:
     void set_use_nra_model(bool m) { m_use_nra_model = m; }
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
+private:
+    void restore_patched_values();
 };  // end of core
 
 struct pp_mon {