From 20c02f4f45c4d04545ff74780904e82ee5d8ae8f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 20 Sep 2023 17:02:35 -0700
Subject: [PATCH 01/12] fix a lambda bug

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/bound_analyzer_on_row.h | 48 ++++++++++++++---------------
 1 file changed, 23 insertions(+), 25 deletions(-)

diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 074b6e464..576f14599 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -281,15 +281,32 @@ private:
     //     */
     // }
 
-    
-    void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
+    void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
+    {
         unsigned row_index = this->m_row_index;
-        auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index,this]() {
-            return explain_bound_on_var_on_coeff((B*)&m_bp, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index);
+        auto* lar = &m_bp.lp();
+        auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
+            TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
+            int bound_sign = (is_lower_bound ? 1 : -1);
+            int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
+
+            SASSERT(!tv::is_term(bound_j));
+            u_dependency* ret = nullptr;
+            for (auto const& r : lar->get_row(row_index)) {
+                unsigned j = r.var();
+                if (j == bound_j)
+                    continue;
+                mpq const& a = r.coeff();
+                int a_sign = is_pos(a) ? 1 : -1;
+                int sign = j_sign * a_sign;
+                u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j);
+                ret = lar->join_deps(ret, witness);
+            }
+            return ret;
         };
         m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain);
     }
-    
+
     void advance_u(unsigned j) {
         m_column_of_u = (m_column_of_u == -1) ? j : -2;
     }
@@ -320,26 +337,7 @@ private:
             break;
         }
     }   
-    static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
-        TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
-        auto& lar = bp->lp();
-        int bound_sign = (is_lower_bound ? 1 : -1);
-        int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
-
-        SASSERT(!tv::is_term(bound_j));
-        u_dependency* ret = nullptr;
-        for (auto const& r : lar.get_row(row_index)) {
-            unsigned j = r.var();
-            if (j == bound_j)
-                continue;
-            mpq const& a = r.coeff();
-            int a_sign = is_pos(a) ? 1 : -1;
-            int sign = j_sign * a_sign;
-            u_dependency* witness = sign > 0 ? lar.get_column_upper_bound_witness(j) : lar.get_column_lower_bound_witness(j);
-            ret = lar.join_deps(ret, witness);
-        }
-        return ret;
-    }
+    
 };
    
 

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 02/12] 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),

From e31cecf5dbe7b6d0542434451e8ed64497bd3075 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 21 Sep 2023 11:27:53 -0700
Subject: [PATCH 03/12] transfer propagate monomial bounds to nla_solver

---
 src/math/lp/lp_bound_propagator.h | 165 -----------------------
 src/math/lp/nla_core.cpp          | 213 +++++++++++++++++++++++++++++-
 src/math/lp/nla_core.h            |  22 ++-
 src/math/lp/nla_solver.cpp        |  11 +-
 src/math/lp/nla_solver.h          |   4 +-
 src/sat/smt/arith_internalize.cpp |   2 +-
 src/smt/theory_lra.cpp            |   9 +-
 7 files changed, 243 insertions(+), 183 deletions(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 99755f606..7ed872aa2 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -120,171 +120,6 @@ public:
         m_column_types = &lp().get_column_types();
     }
    
-    bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
-        zero_var = non_fixed = null_lpvar;
-        unsigned n_of_non_fixed = 0;
-        for (lpvar v : m) {
-            if (!this->column_is_fixed(v)) {
-                n_of_non_fixed++;
-                non_fixed = v;
-                continue;                
-            } 
-            const auto & b = get_lower_bound(v).x;
-            if (b.is_zero()) {
-                zero_var = v;
-                return true;
-            } 
-            
-        }
-        return n_of_non_fixed <= 1;
-    }
-
-    void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
-        auto& lps = lp();
-        auto lambda = [zero_var,&lps]() {
-            return lps.get_bound_constraint_witnesses_for_column(zero_var);
-        };
-        TRACE("add_bound", lp().print_column_info(zero_var, tout) << std::endl;);      
-        add_lower_bound_monic(monic_var, mpq(0), false, lambda);
-        add_upper_bound_monic(monic_var, mpq(0), false, lambda);
-    }
-
-    void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {
-       TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
-       j = lp().column_to_reported_index(j);
-       unsigned k;
-       if (!m_improved_lower_bounds.find(j, k)) {
-            m_improved_lower_bounds.insert(j,static_cast<unsigned>(m_ibounds.size()));
-            m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep));
-       }
-       else {
-            auto& found_bound = m_ibounds[k];
-            if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
-                found_bound = implied_bound(v, j, true, is_strict, explain_dep);
-                TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
-            }
-       }
-    }
-
-    void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function <u_dependency* ()> explain_bound) {
-        j = lp().column_to_reported_index(j);
-        unsigned k;
-        if (!m_improved_upper_bounds.find(j, k)) {
-            m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_ibounds.size()));
-            m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound));
-        }
-        else {
-            auto& found_bound = m_ibounds[k];
-            if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
-                found_bound = implied_bound(bound_val, j, false, is_strict, explain_bound);
-                TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
-            }
-       }
-    }
-
-    void propagate_monic(lpvar monic_var, const svector<lpvar>& vars) {
-        lpvar non_fixed, zero_var;
-        if (!is_linear(vars, zero_var, non_fixed)) 
-            return;
-        
-        if (zero_var != null_lpvar) 
-            add_bounds_for_zero_var(monic_var, zero_var);
-        else {
-            rational k = rational(1);
-            for (auto v : vars)
-                if (v != non_fixed) {
-                    k *= lp().get_column_value(v).x;
-                    if (k.is_big()) return;
-                }
-            
-            if (non_fixed != null_lpvar) 
-                propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
-            else   // all variables are fixed
-                propagate_monic_with_all_fixed(monic_var, vars, k);
-        }
-    }
-    
-    void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
-        lp::impq bound_value;
-        bool is_strict;
-        auto& lps = lp();
-
-        if (lower_bound_is_available(non_fixed)) {
-            bound_value = lp().column_lower_bound(non_fixed);
-            is_strict = !bound_value.y.is_zero();
-            auto lambda = [vars, non_fixed,&lps]() {
-                u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
-                for (auto v : vars) 
-                    if (v != non_fixed) 
-                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                return dep;
-            };
-            if (k.is_pos())
-                add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-            else
-                add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-       }
-
-       if (upper_bound_is_available(non_fixed)) {
-            bound_value = lp().column_upper_bound(non_fixed);
-            is_strict = !bound_value.y.is_zero();
-            auto lambda = [vars, non_fixed,&lps]() {
-                u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
-                for (auto v : vars) 
-                    if (v != non_fixed) 
-                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                return dep;
-            };
-            if (k.is_neg())
-                add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-            else
-                add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-       }
-
-       if (lower_bound_is_available(monic_var)) {
-           auto lambda = [vars, monic_var, non_fixed,&lps]() {
-               u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
-               for (auto v : vars) {
-                   if (v != non_fixed) {
-                       dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                   }
-               }
-               return dep;
-           };
-           bound_value = lp().column_lower_bound(monic_var);
-           is_strict = !bound_value.y.is_zero();
-           if (k.is_pos())
-               add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-           else
-               add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-       }
-       
-       if (upper_bound_is_available(monic_var)) {
-            bound_value = lp().column_upper_bound(monic_var);
-            is_strict = !bound_value.y.is_zero();
-            auto lambda = [vars, monic_var, non_fixed,&lps]() {
-                u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
-                for (auto v : vars) {
-                    if (v != non_fixed) {
-                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                    }
-                }
-                return dep;
-            };
-            if (k.is_neg())
-                add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-            else
-                add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-       }
-    }
-
-    void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k) {
-        auto& lps = lp();
-        auto lambda = [vars,&lps]() { return lps.get_bound_constraint_witnesses_for_columns(vars); };
-        add_lower_bound_monic(monic_var, k, false, lambda);
-        add_upper_bound_monic(monic_var, k, false, lambda);
-    }
-
     column_type get_column_type(unsigned j) const {
         return (*m_column_types)[j];
     }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 63dd29d9b..4e16793ec 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -17,11 +17,12 @@ Author:
 #include "math/grobner/pdd_solver.h"
 #include "math/dd/pdd_interval.h"
 #include "math/dd/pdd_eval.h"
+#include "nla_core.h"
 namespace nla {
 
 typedef lp::lar_term term;
 
-core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim) : m_evars(),
+core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp::implied_bound>& implied_bounds) : m_evars(),
                                                                     lra(s),
                                                                     m_reslim(lim),
                                                                     m_params(p),
@@ -37,7 +38,8 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim) : m_evars(),
                                                                     m_grobner(this),
                                                                     m_emons(m_evars),
                                                                     m_use_nra_model(false),
-                                                                    m_nra(s, m_nra_lim, *this) {
+                                                                    m_nra(s, m_nra_lim, *this),
+                                                                    m_implied_bounds(implied_bounds) {
     m_nlsat_delay = lp_settings().nlsat_delay();
     lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
     for (const auto& m : m_emons) {
@@ -1837,5 +1839,210 @@ bool core::improve_bounds() {
     return bounds_improved;
 }
 
-} // end of nla
+bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
+{
+    zero_var = non_fixed = null_lpvar;
+    unsigned n_of_non_fixed = 0;
+    for (lpvar v : m) {
+        if (!this->var_is_fixed(v)) {
+            n_of_non_fixed++;
+            non_fixed = v;
+            continue;
+        }
+        const auto& b = get_lower_bound(v);
+        if (b.is_zero()) {
+            zero_var = v;
+            return true;
+        }
+    }
+    return n_of_non_fixed <= 1;
+}
+
+void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep)
+{
+    TRACE("add_bound", lra.print_column_info(j, tout) << std::endl;);
+    j = lra.column_to_reported_index(j);
+    unsigned k;
+    if (!m_improved_lower_bounds.find(j, k)) {
+        m_improved_lower_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
+        m_implied_bounds.push_back(lp::implied_bound(v, j, true, is_strict, explain_dep));
+    }
+    else {
+        auto& found_bound = m_implied_bounds[k];
+        if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
+            found_bound = lp::implied_bound(v, j, true, is_strict, explain_dep);
+            TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
+        }
+    }
+}
+
+void core::add_upper_bound_monic(lpvar j, const lp::mpq& bound_val, bool is_strict, std::function<u_dependency*()> explain_dep)
+{
+    j = lra.column_to_reported_index(j);
+    unsigned k;
+    if (!m_improved_upper_bounds.find(j, k)) {
+        m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
+        m_implied_bounds.push_back(lp::implied_bound(bound_val, j, false, is_strict, explain_dep));
+    }
+    else {
+        auto& found_bound = m_implied_bounds[k];
+        if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
+            found_bound = lp::implied_bound(bound_val, j, false, is_strict, explain_dep);
+            TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
+        }
+    }
+}
+
+bool core::upper_bound_is_available(unsigned j) const
+{
+    switch (get_column_type(j)) {
+        case lp::column_type::fixed:
+        case lp::column_type::boxed:
+        case lp::column_type::upper_bound:
+            return true;
+        default:
+            return false;
+    }
+}
+
+bool core::lower_bound_is_available(unsigned j) const
+{
+    switch (get_column_type(j)) {
+        case lp::column_type::fixed:
+        case lp::column_type::boxed:
+        case lp::column_type::lower_bound:
+            return true;
+        default:
+            return false;
+    }
+}
+
+void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
+{
+    lp::impq bound_value;
+    bool is_strict;
+    auto& lps = lra;
+
+    if (lower_bound_is_available(non_fixed)) {
+        bound_value = lra.column_lower_bound(non_fixed);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
+            for (auto v : vars)
+                if (v != non_fixed)
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+            return dep;
+        };
+        if (k.is_pos())
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+    }
+
+    if (upper_bound_is_available(non_fixed)) {
+        bound_value = lra.column_upper_bound(non_fixed);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
+            for (auto v : vars)
+                if (v != non_fixed)
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+    }
+
+    if (lower_bound_is_available(monic_var)) {
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        bound_value = lra.column_lower_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        if (k.is_pos())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    }
+
+    if (upper_bound_is_available(monic_var)) {
+        bound_value = lra.column_upper_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    }
+}
+
+void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
+{
+    auto* lps = &lra;
+    auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
+    add_lower_bound_monic(monic_var, k, false, lambda);
+    add_upper_bound_monic(monic_var, k, false, lambda);
+}
+
+void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var)
+{
+    auto* lps = &lra;
+    auto lambda = [zero_var, lps]() {
+        return lps->get_bound_constraint_witnesses_for_column(zero_var);
+    };
+    TRACE("add_bound", lra.print_column_info(zero_var, tout) << std::endl;);
+    add_lower_bound_monic(monic_var, lp::mpq(0), false, lambda);
+    add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda);
+}
+
+void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var)
+{
+    lpvar non_fixed, zero_var;
+    const auto& vars = m_emons[monic_var].vars();
+    if (!is_linear(vars, zero_var, non_fixed))
+        return;
+
+    if (zero_var != null_lpvar)
+        add_bounds_for_zero_var(monic_var, zero_var);
+    else {
+        rational k = rational(1);
+        for (auto v : vars)
+            if (v != non_fixed) {
+                k *= val(v);
+                if (k.is_big()) return;
+            }
+
+        if (non_fixed != null_lpvar)
+            propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
+        else  // all variables are fixed
+            propagate_monic_with_all_fixed(monic_var, vars, k);
+    }
+}
+
+void core::init_bound_propagation()
+{
+    this->m_implied_bounds.clear();
+    this->m_improved_lower_bounds.reset();
+    this->m_improved_upper_bounds.reset();
+    this->m_column_types = &lra.get_column_types();
+}
+
+}  // namespace nla
+
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 3b888f8ef..54c7e1df1 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -103,7 +103,10 @@ class core {
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable indexed_uint_set m_active_var_set;
-
+    // these maps map a column index to the corresponding index in ibounds
+    u_map<unsigned>          m_improved_lower_bounds;
+    u_map<unsigned>          m_improved_upper_bounds;
+    const vector<lp::column_type>* m_column_types;
     reslimit                 m_nra_lim;
 
     bool                     m_use_nra_model = false;
@@ -114,12 +117,13 @@ class core {
 
     void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
     void add_bounds();
+    std_vector<lp::implied_bound> & m_implied_bounds;
     // try to improve bounds for variables in monomials.
     bool improve_bounds();
 
 public:    
     // constructor
-    core(lp::lar_solver& s, params_ref const& p, reslimit&);
+    core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds);
     const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
     void reset_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
     void insert_to_refine(lpvar j);
@@ -431,15 +435,23 @@ public:
     void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
+    bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed);
+    void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var);
+    void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);
+    void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k);
+    void add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);
+    void add_upper_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);    
+    bool upper_bound_is_available(unsigned j) const;
+    bool lower_bound_is_available(unsigned j) const;
 private:
-    void restore_patched_values();
+    lp::column_type get_column_type(unsigned j) const { return (*m_column_types)[j]; }
     void constrain_nl_in_tableau();
     bool solve_tableau();
     void restore_tableau();
     void save_tableau();
     bool integrality_holds();
-
-
+    void calculate_implied_bounds_for_monic(lp::lpvar v);
+    void init_bound_propagation();    
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 8be918f01..3475a3509 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -54,8 +54,8 @@ namespace nla {
         m_core->pop(n);
     }
     
-    solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit): 
-        m_core(alloc(core, s, p, limit)) {
+    solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds): 
+        m_core(alloc(core, s, p, limit, implied_bounds)) {
     }
     
     bool solver::influences_nl_var(lpvar j) const {    
@@ -88,6 +88,9 @@ namespace nla {
         m_core->collect_statistics(st);
     }
 
+    void solver::calculate_implied_bounds_for_monic(lp::lpvar v) {
+        m_core->calculate_implied_bounds_for_monic(v);
+    }
     // ensure r = x^y, add abstraction/refinement lemmas
     lbool solver::check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
         return m_core->check_power(r, x, y, lemmas);
@@ -97,4 +100,8 @@ namespace nla {
         m_core->check_bounded_divisions(lemmas);
     }
 
+    void solver::init_bound_propagation() {
+        m_core->init_bound_propagation();
+    }
+
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 07bf095a6..a4de90320 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -24,7 +24,7 @@ namespace nla {
         core* m_core;
     public:
 
-        solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
+        solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
         ~solver();
         const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); }
         void reset_monics_with_changed_bounds() { m_core->reset_monics_with_changed_bounds(); } 
@@ -48,5 +48,7 @@ namespace nla {
         nlsat::anum_manager& am();
         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();
     };
 }
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 3174ad775..5893c8520 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -61,7 +61,7 @@ namespace arith {
 
     void solver::ensure_nla() {
         if (!m_nla) {
-            m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit());
+            m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit(), m_implied_bounds);
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nla->push();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index aeb138d3c..ef7ab7091 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -264,7 +264,7 @@ class theory_lra::imp {
 
     void ensure_nla() {
         if (!m_nla) {
-            m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
+            m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit(), m_implied_bounds);
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nla->push();
@@ -2198,13 +2198,10 @@ public:
             finish_bound_propagation();
     }
     
-    void calculate_implied_bounds_for_monic(lpvar monic_var, const svector<lpvar>& vars) {
-        m_bp.propagate_monic(monic_var, vars);
-    }
-    
     void propagate_bounds_for_touched_monomials() {
+        m_nla->init_bound_propagation();
         for (unsigned v : m_nla->monics_with_changed_bounds()) {
-            calculate_implied_bounds_for_monic(v, m_nla->get_core().emons()[v].vars());
+            m_nla->calculate_implied_bounds_for_monic(v);
         }
         m_nla->reset_monics_with_changed_bounds();
     }

From f423642e9b609eb4206519ef95cff4abff3910b1 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 21 Sep 2023 12:18:21 -0700
Subject: [PATCH 04/12] try the lemma scheme

---
 src/math/lp/nla_core.cpp   | 182 +++++++++++++------------------------
 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     |   5 +-
 5 files changed, 72 insertions(+), 123 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 4e16793ec..514b2ad61 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1844,7 +1844,7 @@ bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
     zero_var = non_fixed = null_lpvar;
     unsigned n_of_non_fixed = 0;
     for (lpvar v : m) {
-        if (!this->var_is_fixed(v)) {
+        if (!var_is_fixed(v)) {
             n_of_non_fixed++;
             non_fixed = v;
             continue;
@@ -1920,129 +1920,75 @@ bool core::lower_bound_is_available(unsigned j) const
 void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
 {
     lp::impq bound_value;
-    bool is_strict;
-    auto& lps = lra;
+    new_lemma lemma(*this, "propagate monic with non fixed");
+    // using += to not assert thath the inequality does not hold
+    lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
+    lp::explanation exp;
+    for (auto v : m_emons[monic_var].vars()) {
+        if (v == non_fixed) continue;
+        u_dependency* dep = lra.get_column_lower_bound_witness(v);
+        for (auto ci : lra.flatten(dep)) {
+            exp.push_back(ci);
+        }
+        dep = lra.get_column_upper_bound_witness(v);
+        for (auto ci : lra.flatten(dep)) {
+            exp.push_back(ci);
+        }
+    }
+    lemma &= exp;
+}
 
-    if (lower_bound_is_available(non_fixed)) {
-        bound_value = lra.column_lower_bound(non_fixed);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
+    void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
+    {
+        auto* lps = &lra;
+        auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
+        add_lower_bound_monic(monic_var, k, false, lambda);
+        add_upper_bound_monic(monic_var, k, false, lambda);
+    }
+
+    void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var)
+    {
+        auto* lps = &lra;
+        auto lambda = [zero_var, lps]() {
+            return lps->get_bound_constraint_witnesses_for_column(zero_var);
+        };
+        TRACE("add_bound", lra.print_column_info(zero_var, tout) << std::endl;);
+        add_lower_bound_monic(monic_var, lp::mpq(0), false, lambda);
+        add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda);
+    }
+
+    void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var)
+    {
+        lpvar non_fixed, zero_var;
+        const auto& vars = m_emons[monic_var].vars();
+        if (!is_linear(vars, zero_var, non_fixed))
+            return;
+
+        if (zero_var != null_lpvar)
+            add_bounds_for_zero_var(monic_var, zero_var);
+        else {
+            rational k = rational(1);
             for (auto v : vars)
-                if (v != non_fixed)
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-            return dep;
-        };
-        if (k.is_pos())
-            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-        else
-            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-    }
-
-    if (upper_bound_is_available(non_fixed)) {
-        bound_value = lra.column_upper_bound(non_fixed);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
-            for (auto v : vars)
-                if (v != non_fixed)
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-            return dep;
-        };
-        if (k.is_neg())
-            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-        else
-            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-    }
-
-    if (lower_bound_is_available(monic_var)) {
-        auto lambda = [vars, monic_var, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
-            for (auto v : vars) {
                 if (v != non_fixed) {
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                    k *= val(v);
+                    if (k.is_big()) return;
                 }
-            }
-            return dep;
-        };
-        bound_value = lra.column_lower_bound(monic_var);
-        is_strict = !bound_value.y.is_zero();
-        if (k.is_pos())
-            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-        else
-            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+
+            if (non_fixed != null_lpvar)
+                propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
+            else  // all variables are fixed
+                propagate_monic_with_all_fixed(monic_var, vars, k);
+        }
     }
 
-    if (upper_bound_is_available(monic_var)) {
-        bound_value = lra.column_upper_bound(monic_var);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, monic_var, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
-            for (auto v : vars) {
-                if (v != non_fixed) {
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-                }
-            }
-            return dep;
-        };
-        if (k.is_neg())
-            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-        else
-            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    void core::init_bound_propagation(vector<lemma> & l_vec)
+    {
+        m_implied_bounds.clear();
+        m_improved_lower_bounds.reset();
+        m_improved_upper_bounds.reset();
+        m_column_types = &lra.get_column_types();
+        m_lemma_vec = &l_vec;
+        m_lemma_vec->clear();
     }
-}
-
-void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
-{
-    auto* lps = &lra;
-    auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
-    add_lower_bound_monic(monic_var, k, false, lambda);
-    add_upper_bound_monic(monic_var, k, false, lambda);
-}
-
-void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var)
-{
-    auto* lps = &lra;
-    auto lambda = [zero_var, lps]() {
-        return lps->get_bound_constraint_witnesses_for_column(zero_var);
-    };
-    TRACE("add_bound", lra.print_column_info(zero_var, tout) << std::endl;);
-    add_lower_bound_monic(monic_var, lp::mpq(0), false, lambda);
-    add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda);
-}
-
-void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var)
-{
-    lpvar non_fixed, zero_var;
-    const auto& vars = m_emons[monic_var].vars();
-    if (!is_linear(vars, zero_var, non_fixed))
-        return;
-
-    if (zero_var != null_lpvar)
-        add_bounds_for_zero_var(monic_var, zero_var);
-    else {
-        rational k = rational(1);
-        for (auto v : vars)
-            if (v != non_fixed) {
-                k *= val(v);
-                if (k.is_big()) return;
-            }
-
-        if (non_fixed != null_lpvar)
-            propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
-        else  // all variables are fixed
-            propagate_monic_with_all_fixed(monic_var, vars, k);
-    }
-}
-
-void core::init_bound_propagation()
-{
-    this->m_implied_bounds.clear();
-    this->m_improved_lower_bounds.reset();
-    this->m_improved_upper_bounds.reset();
-    this->m_column_types = &lra.get_column_types();
-}
 
 }  // namespace nla
-
-
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 54c7e1df1..456709771 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<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..08c1e1e62 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<lemma>& lemmas) {
+        m_core->init_bound_propagation(lemmas);
     }
 
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index a4de90320..fa206ea40 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<lemma>&);
     };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ef7ab7091..ea1dcd9b9 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2199,11 +2199,14 @@ 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);
         }
         m_nla->reset_monics_with_changed_bounds();
+        for (const auto & l:m_nla_lemma_vector) {
+            false_case_of_check_nla(l);
+        }
     }
 
     void propagate_bounds_with_nlp() {

From c0b55d14352fa76f3a2eabf346a8d20fb93b4e9e Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 21 Sep 2023 15:53:53 -0700
Subject: [PATCH 05/12] reject rows with columns with big numbers for lp bound
 propagation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 08ff3b0d4..dc114e9e0 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -135,9 +135,15 @@ namespace lp {
 
 
     bool lar_solver::row_has_a_big_num(unsigned i) const {
-        for (const auto& c : A_r().m_rows[i]) 
+        for (const auto& c : A_r().m_rows[i])  {
             if (c.coeff().is_big())
                 return true;
+            if (column_has_lower_bound(c.var())&& get_lower_bound(c.var()).x.is_big())
+                return true;
+            if (column_has_upper_bound(c.var())&& get_upper_bound(c.var()).x.is_big())
+                return true;    
+        }
+
         return false;
     }
 

From 576309a16fe8e6d30dd19bebaeaa1bc0b4856b6a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 21 Sep 2023 16:30:43 -0700
Subject: [PATCH 06/12] Revert "reject rows with columns with big numbers for
 lp bound propagation"

This reverts commit c0b55d14352fa76f3a2eabf346a8d20fb93b4e9e.
---
 src/math/lp/lar_solver.cpp | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index dc114e9e0..08ff3b0d4 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -135,15 +135,9 @@ namespace lp {
 
 
     bool lar_solver::row_has_a_big_num(unsigned i) const {
-        for (const auto& c : A_r().m_rows[i])  {
+        for (const auto& c : A_r().m_rows[i]) 
             if (c.coeff().is_big())
                 return true;
-            if (column_has_lower_bound(c.var())&& get_lower_bound(c.var()).x.is_big())
-                return true;
-            if (column_has_upper_bound(c.var())&& get_upper_bound(c.var()).x.is_big())
-                return true;    
-        }
-
         return false;
     }
 

From caa929f01f4ba66f5fcacd4e83c5fe7c7bfe363f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 22 Sep 2023 14:27:26 -0700
Subject: [PATCH 07/12] do not use lemmase in monomial propagation

---
 src/math/lp/nla_core.cpp   | 88 ++++++++++++++++++++++++++++++--------
 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     |  5 +--
 5 files changed, 75 insertions(+), 26 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 514b2ad61..916b80f6c 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1920,22 +1920,76 @@ bool core::lower_bound_is_available(unsigned j) const
 void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
 {
     lp::impq bound_value;
-    new_lemma lemma(*this, "propagate monic with non fixed");
-    // using += to not assert thath the inequality does not hold
-    lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
-    lp::explanation exp;
-    for (auto v : m_emons[monic_var].vars()) {
-        if (v == non_fixed) continue;
-        u_dependency* dep = lra.get_column_lower_bound_witness(v);
-        for (auto ci : lra.flatten(dep)) {
-            exp.push_back(ci);
-        }
-        dep = lra.get_column_upper_bound_witness(v);
-        for (auto ci : lra.flatten(dep)) {
-            exp.push_back(ci);
-        }
+    bool is_strict;
+    auto& lps = lra;
+
+    if (lower_bound_is_available(non_fixed)) {
+        bound_value = lra.column_lower_bound(non_fixed);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
+            for (auto v : vars)
+                if (v != non_fixed)
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+            return dep;
+        };
+        if (k.is_pos())
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+    }
+
+    if (upper_bound_is_available(non_fixed)) {
+        bound_value = lra.column_upper_bound(non_fixed);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
+            for (auto v : vars)
+                if (v != non_fixed)
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        else
+            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+    }
+
+    if (lower_bound_is_available(monic_var)) {
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        bound_value = lra.column_lower_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        if (k.is_pos())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+    }
+
+    if (upper_bound_is_available(monic_var)) {
+        bound_value = lra.column_upper_bound(monic_var);
+        is_strict = !bound_value.y.is_zero();
+        auto lambda = [vars, monic_var, non_fixed, &lps]() {
+            u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
+            for (auto v : vars) {
+                if (v != non_fixed) {
+                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                }
+            }
+            return dep;
+        };
+        if (k.is_neg())
+            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        else
+            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
     }
-    lemma &= exp;
 }
 
     void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
@@ -1981,14 +2035,12 @@ void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>&
         }
     }
 
-    void core::init_bound_propagation(vector<lemma> & l_vec)
+    void core::init_bound_propagation()
     {
         m_implied_bounds.clear();
         m_improved_lower_bounds.reset();
         m_improved_upper_bounds.reset();
         m_column_types = &lra.get_column_types();
-        m_lemma_vec = &l_vec;
-        m_lemma_vec->clear();
     }
 
 }  // namespace nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 456709771..54c7e1df1 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(vector<lemma>&);    
+    void init_bound_propagation();    
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 08c1e1e62..3475a3509 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(vector<lemma>& lemmas) {
-        m_core->init_bound_propagation(lemmas);
+    void solver::init_bound_propagation() {
+        m_core->init_bound_propagation();
     }
 
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index fa206ea40..a4de90320 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(vector<lemma>&);
+        void init_bound_propagation();
     };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ea1dcd9b9..ef7ab7091 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2199,14 +2199,11 @@ public:
     }
     
     void propagate_bounds_for_touched_monomials() {
-        m_nla->init_bound_propagation(m_nla_lemma_vector);
+        m_nla->init_bound_propagation();
         for (unsigned v : m_nla->monics_with_changed_bounds()) {
             m_nla->calculate_implied_bounds_for_monic(v);
         }
         m_nla->reset_monics_with_changed_bounds();
-        for (const auto & l:m_nla_lemma_vector) {
-            false_case_of_check_nla(l);
-        }
     }
 
     void propagate_bounds_with_nlp() {

From 940775d12d1b214bdf010aae4f8476fbbefa9b9b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Sep 2023 16:48:40 -0700
Subject: [PATCH 08/12] indentation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp | 121 +++++++++++++++++++--------------------
 src/smt/smt_context.cpp  |   2 +
 src/smt/theory_lra.cpp   |  15 +++--
 3 files changed, 70 insertions(+), 68 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 514b2ad61..079eccd74 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -22,24 +22,25 @@ namespace nla {
 
 typedef lp::lar_term term;
 
-core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp::implied_bound>& implied_bounds) : m_evars(),
-                                                                    lra(s),
-                                                                    m_reslim(lim),
-                                                                    m_params(p),
-                                                                    m_tangents(this),
-                                                                    m_basics(this),
-                                                                    m_order(this),
-                                                                    m_monotone(this),
-                                                                    m_powers(*this),
-                                                                    m_divisions(*this),
-                                                                    m_intervals(this, lim),
-                                                                    m_monomial_bounds(this),
-                                                                    m_horner(this),
-                                                                    m_grobner(this),
-                                                                    m_emons(m_evars),
-                                                                    m_use_nra_model(false),
-                                                                    m_nra(s, m_nra_lim, *this),
-                                                                    m_implied_bounds(implied_bounds) {
+core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp::implied_bound>& implied_bounds) :
+    m_evars(),
+    lra(s),
+    m_reslim(lim),
+    m_params(p),
+    m_tangents(this),
+    m_basics(this),
+    m_order(this),
+    m_monotone(this),
+    m_powers(*this),
+    m_divisions(*this),
+    m_intervals(this, lim),
+    m_monomial_bounds(this),
+    m_horner(this),
+    m_grobner(this),
+    m_emons(m_evars),
+    m_use_nra_model(false),
+    m_nra(s, m_nra_lim, *this),
+    m_implied_bounds(implied_bounds) {
     m_nlsat_delay = lp_settings().nlsat_delay();
     lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
     for (const auto& m : m_emons) {
@@ -1839,8 +1840,7 @@ bool core::improve_bounds() {
     return bounds_improved;
 }
 
-bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
-{
+bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
     zero_var = non_fixed = null_lpvar;
     unsigned n_of_non_fixed = 0;
     for (lpvar v : m) {
@@ -1858,8 +1858,7 @@ bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
     return n_of_non_fixed <= 1;
 }
 
-void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep)
-{
+void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {
     TRACE("add_bound", lra.print_column_info(j, tout) << std::endl;);
     j = lra.column_to_reported_index(j);
     unsigned k;
@@ -1876,67 +1875,63 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
     }
 }
 
-void core::add_upper_bound_monic(lpvar j, const lp::mpq& bound_val, bool is_strict, std::function<u_dependency*()> explain_dep)
-{
-    j = lra.column_to_reported_index(j);
-    unsigned k;
-    if (!m_improved_upper_bounds.find(j, k)) {
-        m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
-        m_implied_bounds.push_back(lp::implied_bound(bound_val, j, false, is_strict, explain_dep));
-    }
-    else {
-        auto& found_bound = m_implied_bounds[k];
-        if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
-            found_bound = lp::implied_bound(bound_val, j, false, is_strict, explain_dep);
-            TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
+    void core::add_upper_bound_monic(lpvar j, const lp::mpq& bound_val, bool is_strict, std::function<u_dependency*()> explain_dep) {
+        j = lra.column_to_reported_index(j);
+        unsigned k;
+        if (!m_improved_upper_bounds.find(j, k)) {
+            m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_implied_bounds.size()));
+            m_implied_bounds.push_back(lp::implied_bound(bound_val, j, false, is_strict, explain_dep));
+        }
+        else {
+            auto& found_bound = m_implied_bounds[k];
+            if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
+                found_bound = lp::implied_bound(bound_val, j, false, is_strict, explain_dep);
+                TRACE("add_bound", lra.print_implied_bound(found_bound, tout););
+            }
         }
     }
-}
 
-bool core::upper_bound_is_available(unsigned j) const
-{
-    switch (get_column_type(j)) {
+    bool core::upper_bound_is_available(unsigned j) const {
+        switch (get_column_type(j)) {
         case lp::column_type::fixed:
         case lp::column_type::boxed:
         case lp::column_type::upper_bound:
             return true;
         default:
             return false;
+        }
     }
-}
-
-bool core::lower_bound_is_available(unsigned j) const
-{
-    switch (get_column_type(j)) {
+    
+    bool core::lower_bound_is_available(unsigned j) const {
+        switch (get_column_type(j)) {
         case lp::column_type::fixed:
         case lp::column_type::boxed:
         case lp::column_type::lower_bound:
             return true;
         default:
             return false;
+        }
     }
-}
 
-void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
-{
-    lp::impq bound_value;
-    new_lemma lemma(*this, "propagate monic with non fixed");
-    // using += to not assert thath the inequality does not hold
-    lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
-    lp::explanation exp;
-    for (auto v : m_emons[monic_var].vars()) {
-        if (v == non_fixed) continue;
-        u_dependency* dep = lra.get_column_lower_bound_witness(v);
-        for (auto ci : lra.flatten(dep)) {
-            exp.push_back(ci);
-        }
-        dep = lra.get_column_upper_bound_witness(v);
-        for (auto ci : lra.flatten(dep)) {
-            exp.push_back(ci);
+    void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
+        lp::impq bound_value;
+        new_lemma lemma(*this, "propagate monic with non fixed");
+        // using += to not assert thath the inequality does not hold
+        lemma += ineq(term(rational(1), monic_var, -k, non_fixed), llc::EQ, 0);
+        lp::explanation exp;
+        for (auto v : m_emons[monic_var].vars()) {
+            if (v == non_fixed) continue;
+            u_dependency* dep = lra.get_column_lower_bound_witness(v);
+            for (auto ci : lra.flatten(dep)) {
+                exp.push_back(ci);
+            }
+            dep = lra.get_column_upper_bound_witness(v);
+            for (auto ci : lra.flatten(dep)) {
+                exp.push_back(ci);
+            }
         }
+        lemma &= exp;
     }
-    lemma &= exp;
-}
 
     void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
     {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 64c7bbf2e..a3cd99e37 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4522,6 +4522,8 @@ namespace smt {
             theory_var_list * l = n->get_th_var_list();
             theory_id th_id     = l->get_id();
 
+            verbose_stream() << "num parents " << n->get_num_parents() << "\n";
+
             for (enode * parent : enode::parents(n)) {
                 app* p = parent->get_expr();
                 family_id fid = p->get_family_id();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ea1dcd9b9..beec02d98 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1480,6 +1480,7 @@ public:
         m_model_eqs.reset();
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
+        verbose_stream() << "check " << sz << "\n";
         for (theory_var v = 0; v < sz; ++v) {
             enode * n1 = get_enode(v);
             if (!th.is_relevant_and_shared(n1)) {
@@ -1528,12 +1529,16 @@ public:
         unsigned old_sz = m_assume_eq_candidates.size();
         unsigned num_candidates = 0;
         int start = ctx().get_random_value();
+        verbose_stream() << "assume-eqs " << sz << "\n";
+        unsigned num_relevant = 0;
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
+            verbose_stream() << enode_pp(n1, ctx()) << "\n";
             if (!th.is_relevant_and_shared(n1)) {                    
                 continue;
             }
+            ++num_relevant;
             ensure_column(v);
             if (!is_registered_var(v))
                 continue;
@@ -1551,7 +1556,8 @@ public:
                 num_candidates++;
             }
         }
-            
+
+        verbose_stream() << "candidates " << num_candidates << " num relevant " << num_relevant << "\n";
         if (num_candidates > 0) {
             ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         }
@@ -2200,13 +2206,12 @@ public:
     
     void propagate_bounds_for_touched_monomials() {
         m_nla->init_bound_propagation(m_nla_lemma_vector);
-        for (unsigned v : m_nla->monics_with_changed_bounds()) {
+        for (unsigned v : m_nla->monics_with_changed_bounds()) 
             m_nla->calculate_implied_bounds_for_monic(v);
-        }
+        
         m_nla->reset_monics_with_changed_bounds();
-        for (const auto & l:m_nla_lemma_vector) {
+        for (const auto & l : m_nla_lemma_vector) 
             false_case_of_check_nla(l);
-        }
     }
 
     void propagate_bounds_with_nlp() {

From 886d3f43511eb997dc16607daa24c75456f57532 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Sep 2023 16:55:34 -0700
Subject: [PATCH 09/12] indentation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp | 151 +++++++++++++++++++--------------------
 1 file changed, 73 insertions(+), 78 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 904da26cd..38f741388 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1913,91 +1913,88 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
         }
     }
 
-void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k)
-{
-    lp::impq bound_value;
-    bool is_strict;
-    auto& lps = lra;
+    void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
+        lp::impq bound_value;
+        bool is_strict;
+        auto& lps = lra;
+        
+        if (lower_bound_is_available(non_fixed)) {
+            bound_value = lra.column_lower_bound(non_fixed);
+            is_strict = !bound_value.y.is_zero();
+            auto lambda = [vars, non_fixed, &lps]() {
+                u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
+                for (auto v : vars)
+                    if (v != non_fixed)
+                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                return dep;
+            };
+            if (k.is_pos())
+                add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+            else
+                add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        }
+        
+        if (upper_bound_is_available(non_fixed)) {
+            bound_value = lra.column_upper_bound(non_fixed);
+            is_strict = !bound_value.y.is_zero();
+            auto lambda = [vars, non_fixed, &lps]() {
+                u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
+                for (auto v : vars)
+                    if (v != non_fixed)
+                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                return dep;
+            };
+            if (k.is_neg())
+                add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+            else
+                add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
+        }
 
-    if (lower_bound_is_available(non_fixed)) {
-        bound_value = lra.column_lower_bound(non_fixed);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
-            for (auto v : vars)
-                if (v != non_fixed)
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-            return dep;
-        };
-        if (k.is_pos())
-            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-        else
-            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-    }
-
-    if (upper_bound_is_available(non_fixed)) {
-        bound_value = lra.column_upper_bound(non_fixed);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
-            for (auto v : vars)
-                if (v != non_fixed)
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
-            return dep;
-        };
-        if (k.is_neg())
-            add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-        else
-            add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
-    }
-
-    if (lower_bound_is_available(monic_var)) {
-        auto lambda = [vars, monic_var, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
-            for (auto v : vars) {
-                if (v != non_fixed) {
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+        if (lower_bound_is_available(monic_var)) {
+            auto lambda = [vars, monic_var, non_fixed, &lps]() {
+                u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
+                for (auto v : vars) {
+                    if (v != non_fixed) {
+                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                    }
                 }
-            }
-            return dep;
-        };
-        bound_value = lra.column_lower_bound(monic_var);
-        is_strict = !bound_value.y.is_zero();
-        if (k.is_pos())
-            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-        else
-            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-    }
-
-    if (upper_bound_is_available(monic_var)) {
-        bound_value = lra.column_upper_bound(monic_var);
-        is_strict = !bound_value.y.is_zero();
-        auto lambda = [vars, monic_var, non_fixed, &lps]() {
-            u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
-            for (auto v : vars) {
-                if (v != non_fixed) {
-                    dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                return dep;
+            };
+            bound_value = lra.column_lower_bound(monic_var);
+            is_strict = !bound_value.y.is_zero();
+            if (k.is_pos())
+                add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+            else
+                add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        }
+        
+        if (upper_bound_is_available(monic_var)) {
+            bound_value = lra.column_upper_bound(monic_var);
+            is_strict = !bound_value.y.is_zero();
+            auto lambda = [vars, monic_var, non_fixed, &lps]() {
+                u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
+                for (auto v : vars) {
+                    if (v != non_fixed) {
+                        dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
+                    }
                 }
-            }
-            return dep;
-        };
-        if (k.is_neg())
-            add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
-        else
-            add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+                return dep;
+            };
+            if (k.is_neg())
+                add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+            else
+                add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
+        }
     }
-}
 
-    void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k)
-    {
+    void core::propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k) {
         auto* lps = &lra;
         auto lambda = [vars, lps]() { return lps->get_bound_constraint_witnesses_for_columns(vars); };
         add_lower_bound_monic(monic_var, k, false, lambda);
         add_upper_bound_monic(monic_var, k, false, lambda);
     }
 
-    void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var)
-    {
+    void core::add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
         auto* lps = &lra;
         auto lambda = [zero_var, lps]() {
             return lps->get_bound_constraint_witnesses_for_column(zero_var);
@@ -2007,8 +2004,7 @@ void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>&
         add_upper_bound_monic(monic_var, lp::mpq(0), false, lambda);
     }
 
-    void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var)
-    {
+    void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var) {
         lpvar non_fixed, zero_var;
         const auto& vars = m_emons[monic_var].vars();
         if (!is_linear(vars, zero_var, non_fixed))
@@ -2031,8 +2027,7 @@ void core::propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>&
         }
     }
 
-    void core::init_bound_propagation()
-    {
+    void core::init_bound_propagation() {
         m_implied_bounds.clear();
         m_improved_lower_bounds.reset();
         m_improved_upper_bounds.reset();

From 421fe946079ffb79ccae99bd85ffc6211c9570f7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 22 Sep 2023 17:59:07 -0700
Subject: [PATCH 10/12] rmove debug out

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 8ffeff3fb..8bf17ec4d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1529,12 +1529,10 @@ public:
         unsigned old_sz = m_assume_eq_candidates.size();
         unsigned num_candidates = 0;
         int start = ctx().get_random_value();
-        verbose_stream() << "assume-eqs " << sz << "\n";
         unsigned num_relevant = 0;
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
-            verbose_stream() << enode_pp(n1, ctx()) << "\n";
             if (!th.is_relevant_and_shared(n1)) {                    
                 continue;
             }
@@ -1557,7 +1555,6 @@ public:
             }
         }
 
-        verbose_stream() << "candidates " << num_candidates << " num relevant " << num_relevant << "\n";
         if (num_candidates > 0) {
             ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         }

From acad9fa62c0cab9089ee385098e50545d544b2bb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Sep 2023 16:25:46 -0700
Subject: [PATCH 11/12] Update smt_context.cpp

---
 src/smt/smt_context.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a3cd99e37..64c7bbf2e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4522,8 +4522,6 @@ namespace smt {
             theory_var_list * l = n->get_th_var_list();
             theory_id th_id     = l->get_id();
 
-            verbose_stream() << "num parents " << n->get_num_parents() << "\n";
-
             for (enode * parent : enode::parents(n)) {
                 app* p = parent->get_expr();
                 family_id fid = p->get_family_id();

From a3e2e68d93dcb4f2891e779fbe4419cc00db2b5e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Sep 2023 16:26:31 -0700
Subject: [PATCH 12/12] Update theory_lra.cpp

---
 src/smt/theory_lra.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 8bf17ec4d..21e021ea7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1480,7 +1480,6 @@ public:
         m_model_eqs.reset();
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
-        verbose_stream() << "check " << sz << "\n";
         for (theory_var v = 0; v < sz; ++v) {
             enode * n1 = get_enode(v);
             if (!th.is_relevant_and_shared(n1)) {