From 536930b4a160cf5e1f7260016629f0a17adc8459 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 20 Sep 2023 17:13:25 -0700
Subject: [PATCH] make m_ibounds inside of lp_bound_propagator  a reference

---
 src/math/lp/lp_bound_propagator.h | 4 ++--
 src/sat/smt/arith_solver.cpp      | 2 +-
 src/sat/smt/arith_solver.h        | 1 +
 src/smt/theory_lra.cpp            | 3 ++-
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index f6cc83825..99755f606 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -20,7 +20,7 @@ class lp_bound_propagator {
     u_map<unsigned> m_improved_upper_bounds;
 
     T& m_imp;
-    std_vector<implied_bound> m_ibounds;
+    std_vector<implied_bound>& m_ibounds;
 
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
     // works for rows of the form x + y + sum of fixed = 0
@@ -109,7 +109,7 @@ private:
     };
 
 public:
-    lp_bound_propagator(T& imp) : m_imp(imp) {}
+    lp_bound_propagator(T& imp, std_vector<implied_bound> & ibounds) : m_imp(imp), m_ibounds(ibounds) {}
 
     const std_vector<implied_bound>& ibounds() const { return m_ibounds; }
 
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index fd55fb7d7..3cf991c20 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -26,7 +26,7 @@ namespace arith {
         m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_local_search(*this),
         m_resource_limit(*this),
-        m_bp(*this),
+        m_bp(*this, m_implied_bounds),
         a(m),
         m_bound_terms(m),
         m_bound_predicate(m)
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index e23162393..8917a3e42 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -243,6 +243,7 @@ namespace arith {
         resource_limit               m_resource_limit;
         lp_bounds                    m_new_bounds;
         symbol                       m_farkas;
+        std_vector<lp::implied_bound> m_implied_bounds;
         lp::lp_bound_propagator<solver> m_bp;
         mutable vector<std::pair<lp::tv, rational>> m_todo_terms;
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9357b7a65..aeb138d3c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -225,6 +225,7 @@ class theory_lra::imp {
     lp_bounds                    m_new_bounds;
     symbol                       m_farkas;
     vector<parameter>            m_bound_params;
+    std_vector<lp::implied_bound>   m_implied_bounds;
     lp::lp_bound_propagator<imp> m_bp;
 
     context& ctx() const { return th.get_context(); }
@@ -873,7 +874,7 @@ public:
         m_solver(nullptr),
         m_resource_limit(*this),
         m_farkas("farkas"),
-        m_bp(*this),
+        m_bp(*this, m_implied_bounds),
         m_bounded_range_idx(0),
         m_bounded_range_lit(null_literal),
         m_bound_terms(m),