From 26a9b776c65076c647f9793fbe512ab43ff46d3e Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 25 Sep 2023 12:10:59 -0700
Subject: [PATCH] clean m_nla_lemma_vector in nla_solver

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

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 38f741388..84367fbbc 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -2027,11 +2027,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
         }
     }
 
-    void core::init_bound_propagation() {
+    void core::init_bound_propagation(vector<nla::lemma>& lemma_vector) {
         m_implied_bounds.clear();
         m_improved_lower_bounds.reset();
         m_improved_upper_bounds.reset();
         m_column_types = &lra.get_column_types();
+        lemma_vector.clear();
     }
 
 }  // namespace nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 54c7e1df1..c561b91c0 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -451,7 +451,7 @@ private:
     void save_tableau();
     bool integrality_holds();
     void calculate_implied_bounds_for_monic(lp::lpvar v);
-    void init_bound_propagation();    
+    void init_bound_propagation(vector<nla::lemma> &);    
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 3475a3509..e8b2d9d1d 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -100,8 +100,8 @@ namespace nla {
         m_core->check_bounded_divisions(lemmas);
     }
 
-    void solver::init_bound_propagation() {
-        m_core->init_bound_propagation();
+    void solver::init_bound_propagation(vector<nla::lemma>& nla_lemma_vector) {
+        m_core->init_bound_propagation(nla_lemma_vector);
     }
 
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index a4de90320..7f52b5c92 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -49,6 +49,6 @@ namespace nla {
         nlsat::anum const& am_value(lp::var_index v) const;
         void collect_statistics(::statistics & st);
         void calculate_implied_bounds_for_monic(lp::lpvar v);
-        void init_bound_propagation();
+        void init_bound_propagation(vector<nla::lemma>&);
     };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 21e021ea7..5405f7ff1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2201,7 +2201,7 @@ public:
     }
     
     void propagate_bounds_for_touched_monomials() {
-        m_nla->init_bound_propagation();
+        m_nla->init_bound_propagation(m_nla_lemma_vector);
         for (unsigned v : m_nla->monics_with_changed_bounds()) 
             m_nla->calculate_implied_bounds_for_monic(v);