From 7de06c4350fa7f387c1823e3c8f0ecdda45249e7 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 2 Oct 2023 16:42:59 -0700
Subject: [PATCH] merging master to unit_prop_on_monomials

---
 src/math/lp/monomial_bounds.cpp      | 166 ++++++++++++++------
 src/math/lp/monomial_bounds.h        |  16 +-
 src/math/lp/nla_core.cpp             | 216 ++++-----------------------
 src/math/lp/nla_core.h               |  49 +++---
 src/math/lp/nla_solver.cpp           |  41 +++--
 src/math/lp/nla_solver.h             |  15 +-
 src/math/lp/nla_types.h              |  15 +-
 src/sat/smt/arith_internalize.cpp    |   2 +-
 src/sat/smt/arith_solver.cpp         |   6 +-
 src/sat/smt/arith_solver.h           |   1 -
 src/sat/smt/euf_proof_checker.cpp    |   6 +-
 src/smt/params/smt_params_helper.pyg |   2 -
 src/smt/smt_clause_proof.cpp         |  22 ++-
 src/smt/smt_clause_proof.h           |   6 +-
 src/smt/smt_conflict_resolution.cpp  |   1 +
 src/smt/smt_internalizer.cpp         |   6 +-
 src/smt/theory_arith_aux.h           |   3 +-
 src/smt/theory_arith_nl.h            |  15 +-
 src/smt/theory_lra.cpp               | 120 ++++++++-------
 19 files changed, 333 insertions(+), 375 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 177cfb3d3..8bb6ab306 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -10,34 +10,9 @@
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_intervals.h"
+#include "math/lp/numeric_pair.h"
 
 namespace nla {
-    // here non_fixed is the only non-fixed variable in the monomial, 
-    // vars is the vector of the monomial variables, 
-    // k is the product of all fixed variables in vars 
-    void monomial_bounds::propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
-        vector<std::pair<lp::mpq, unsigned>> coeffs;        
-        coeffs.push_back(std::make_pair(-k, non_fixed));
-        coeffs.push_back(std::make_pair(rational::one(), monic_var));
-        lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
-        auto* dep = explain_fixed(vars, non_fixed);
-        // term_index becomes the column index of the term slack variable
-        term_index = c().lra.map_term_index_to_column_index(term_index);
-        c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
-        c().lra.track_column_feasibility(term_index);
-        if (!c().lra.column_is_feasible(term_index)) {
-            c().lra.set_status(lp::lp_status::UNKNOWN);
-        }
-        
-    }
-
-    u_dependency* monomial_bounds::explain_fixed(const svector<lpvar>& vars, lpvar non_fixed) {
-        u_dependency* dep = nullptr;
-        for (auto v : vars)
-            if (v != non_fixed)
-                dep = c().lra.join_deps(dep, c().lra.get_bound_constraint_witnesses_for_column(v));
-        return dep;
-    }
 
     monomial_bounds::monomial_bounds(core* c):
         common(c), 
@@ -50,6 +25,7 @@ namespace nla {
         }
     }
 
+
     bool monomial_bounds::is_too_big(mpq const& q) const {
         return rational(q).bitsize() > 256;
     }
@@ -283,25 +259,127 @@ namespace nla {
         }
     }
 
-    // returns true iff  (all variables are fixed,
-    // or all but one variable are fixed) and the bounds are not big,
-    // or at least one variable is fixed to zero.
-    bool monomial_bounds::is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed) {
-        zero_var = non_fixed = null_lpvar;
-        unsigned n_of_non_fixed = 0;
-        bool big_bound = false;
-        for (lpvar v : m) {
-            if (!c().var_is_fixed(v)) {
-                n_of_non_fixed++;
-                non_fixed = v;
-            } else if (c().var_is_fixed_to_zero(v)) {
-                zero_var = v;
-                return true;
-            } else if (c().fixed_var_has_big_bound(v)) {
-                big_bound |= true;
+    void monomial_bounds::unit_propagate() {        
+        for (auto const& m : c().m_emons) {
+            unit_propagate(m);
+            if (c().lra.get_status() == lp::lp_status::INFEASIBLE) {
+                lp::explanation exp;
+                c().lra.get_infeasibility_explanation(exp);
+                new_lemma lemma(c(), "propagate fixed - infeasible lra");
+                lemma &= exp;
+                return;
             }
-        }
-        return n_of_non_fixed <= 1 && !big_bound;
+            if (c().m_conflicts > 0 ) {
+                return;
+            }
+        }   
     }
+
+
+    void monomial_bounds::unit_propagate(monic const& m) {
+        if (m.is_propagated())
+            return;
+
+        if (!is_linear(m))
+            return;
+
+        
+        rational k = fixed_var_product(m);
+        lpvar w = non_fixed_var(m);
+        if (w == null_lpvar || k == 0) {
+            propagate_fixed(m, k);
+        }
+        else
+            propagate_nonfixed(m, k, w);
+    }
+
+    lp::explanation monomial_bounds::get_explanation(u_dependency* dep) {
+        lp::explanation exp;
+        svector<lp::constraint_index> cs;
+        c().lra.dep_manager().linearize(dep, cs);
+        for (auto d : cs)
+            exp.add_pair(d, mpq(1));
+        return exp;
+    }
+
+    void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
+        auto* dep = explain_fixed(m, k);
+        if (!c().lra.is_base(m.var())) {
+            lp::impq val(k);
+            c().lra.set_value_for_nbasic_column(m.var(), val);
+        }
+        c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
+        
+        // propagate fixed equality
+        auto exp = get_explanation(dep);
+        c().add_fixed_equality(m.var(), k, exp);
+    }
+
+    void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
+        VERIFY(k != 0);
+        vector<std::pair<lp::mpq, unsigned>> coeffs;        
+        coeffs.push_back(std::make_pair(-k, w));
+        coeffs.push_back(std::make_pair(rational::one(), m.var()));
+        lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
+        auto* dep = explain_fixed(m, k);
+        term_index = c().lra.map_term_index_to_column_index(term_index);
+        c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
+
+        if (k == 1) {
+            lp::explanation exp = get_explanation(dep);
+            c().add_equality(m.var(), w, exp);
+        }
+    }
+
+    u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) {
+        u_dependency* dep = nullptr;
+        auto update_dep = [&](unsigned j) {
+            dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j));
+            dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j));
+            return dep;
+        };
+
+        if (k == 0) {
+            for (auto j : m.vars()) 
+                if (c().var_is_fixed_to_zero(j)) 
+                    return update_dep(j);
+        }
+        else {
+            for (auto j : m.vars()) 
+                if (c().var_is_fixed(j))
+                    update_dep(j);
+        }
+        return dep;
+    }
+
+    
+    bool monomial_bounds::is_linear(monic const& m) {
+        unsigned non_fixed = 0;
+        for (lpvar v : m) {
+            if (!c().var_is_fixed(v))
+                ++non_fixed;
+            else if (c().val(v).is_zero())
+                return true;
+        }
+        return non_fixed <= 1;
+    }
+    
+    
+    rational monomial_bounds::fixed_var_product(monic const& m) {
+        rational r(1);
+        for (lpvar v : m) {
+            if (c().var_is_fixed(v))
+                r *= c().lra.get_column_value(v).x;
+        }
+        return r;
+    }
+    
+    lpvar monomial_bounds::non_fixed_var(monic const& m) {
+        for (lpvar v : m) 
+            if (!c().var_is_fixed(v))
+                return v;
+        return null_lpvar;
+    }
+
 }
 
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 76524012f..747aca9a2 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -17,24 +17,32 @@ namespace nla {
     class monomial_bounds : common {
         dep_intervals& dep;
 
-        u_dependency* explain_fixed(const svector<lpvar>& vars, lpvar non_fixed);
+
         void var2interval(lpvar v, scoped_dep_interval& i);
         bool is_too_big(mpq const& q) const;
+        bool propagate_down(monic const& m, lpvar u);
         bool propagate_value(dep_interval& range, lpvar v);
         bool propagate_value(dep_interval& range, lpvar v, unsigned power);
         void compute_product(unsigned start, monic const& m, scoped_dep_interval& i);
         bool propagate(monic const& m);
+        void propagate_fixed(monic const& m, rational const& k);
+        void propagate_nonfixed(monic const& m, rational const& k, lpvar w);
+        u_dependency* explain_fixed(monic const& m, rational const& k);
+        lp::explanation get_explanation(u_dependency* dep);
         bool propagate_down(monic const& m, dep_interval& mi, lpvar v, unsigned power, dep_interval& product);
         void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const;
         bool is_free(lpvar v) const;
         bool is_zero(lpvar v) const;
 
         // monomial propagation
-        bool_vector m_propagated;
-        bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed);
+        void unit_propagate(monic const& m);
+        bool is_linear(monic const& m);
+        rational fixed_var_product(monic const& m);
+        lpvar non_fixed_var(monic const& m);
+
     public:
         monomial_bounds(core* core);
         void propagate();
-        void propagate_nonfixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);    
+        void unit_propagate();
     }; 
 }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 5a6af5659..6a241e951 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -17,12 +17,11 @@ 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, std_vector<lp::implied_bound>& implied_bounds) :
+core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     m_evars(),
     lra(s),
     m_reslim(lim),
@@ -39,11 +38,11 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp:
     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();    
+    m_nra(s, m_nra_lim, *this) 
+{
+    m_nlsat_delay = lp_settings().nlsat_delay();
 }
-
+    
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
     switch(cmp) {
     case llc::LE: return ls <= rs;
@@ -138,7 +137,6 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
         m_add_buffer[i] = j;
     }
     m_emons.add(v, m_add_buffer);
-    m_monics_with_changed_bounds.insert(v);
 }
     
 void core::push() {
@@ -543,13 +541,6 @@ bool core::var_is_fixed_to_zero(lpvar j) const {
         lra.column_is_fixed(j) &&
         lra.get_lower_bound(j) == lp::zero_of_type<lp::impq>();
 }
-
-bool core::fixed_var_has_big_bound(lpvar j) const {
-    SASSERT(lra.column_is_fixed(j));
-    const auto& b = lra.get_lower_bound(j);
-    return  b.x.is_big() || b.y.is_big();
-}
-
 bool core::var_is_fixed_to_val(lpvar j, const rational& v) const {
     return 
         lra.column_is_fixed(j) &&
@@ -818,7 +809,10 @@ void core::print_stats(std::ostream& out) {
 
 void core::clear() {
     m_lemmas.clear();
-    m_literal_vec->clear();
+    m_literals.clear();
+    m_fixed_equalities.clear();
+    m_equalities.clear();
+    m_conflicts = 0;
 }
     
 void core::init_search() {
@@ -1065,14 +1059,6 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
     }
     return *this;
 }
-
-// Contrary to new_lemma::operator|=, this method does not assert that the model does not satisfy the ineq.
-new_lemma& new_lemma::operator+=(ineq const& ineq) {
-    if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
-        current().push_back(ineq);
-    }
-    return *this;
-}
     
 
 new_lemma::~new_lemma() {
@@ -1080,6 +1066,9 @@ new_lemma::~new_lemma() {
     (void)i;
     (void)name;
     // code for checking lemma can be added here
+    if (current().is_conflict()) {
+        c.m_conflicts++;
+    }
     TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; );
 }
 
@@ -1511,12 +1500,12 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
 }
 
 lbool core::check_power(lpvar r, lpvar x, lpvar y) {
-    m_lemmas.reset();
+    clear();
     return m_powers.check(r, x, y, m_lemmas);
 }
 
 void core::check_bounded_divisions() {
-    m_lemmas.reset();
+    clear();
     m_divisions.check_bounded_divisions();
 }
 // looking for a free variable inside of a monic to split
@@ -1528,18 +1517,17 @@ void core::add_bounds() {
         for (lpvar j : m.vars()) {
             if (!var_is_free(j)) continue;
             // split the free variable (j <= 0, or j > 0), and return
-            m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));  
+            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));  
             ++lp_settings().stats().m_nla_bounds;
             return;
         }
     }    
 }
 
-lbool core::check(vector<ineq>& lits) {
+lbool core::check() {
     lp_settings().stats().m_nla_calls++;
     TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
     lra.get_rid_of_inf_eps();
-    m_literal_vec = &lits;
     if (!(lra.get_status() == lp::lp_status::OPTIMAL || 
           lra.get_status() == lp::lp_status::FEASIBLE)) {
         TRACE("nla_solver", tout << "unknown because of the lra.m_status = " << lra.get_status() << "\n";);
@@ -1559,7 +1547,7 @@ lbool core::check(vector<ineq>& lits) {
     bool run_bounded_nlsat = should_run_bounded_nlsat();
     bool run_bounds = params().arith_nl_branching();    
 
-    auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); };
+    auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty(); };
     
     if (no_effect())
         m_monomial_bounds.propagate();
@@ -1577,7 +1565,7 @@ lbool core::check(vector<ineq>& lits) {
               {1, check2},
               {1, check3} };
         check_weighted(3, checks);
-        if (!m_lemmas.empty() || !lits.empty())
+        if (!m_lemmas.empty() || !m_literals.empty())
             return l_false;
     }
                 
@@ -1656,9 +1644,8 @@ lbool core::bounded_nlsat() {
         m_nlsat_fails = 0;
         m_nlsat_delay /= 2;
     }
-    if (ret == l_true) {
-        m_lemmas.reset();
-    }
+    if (ret == l_true) 
+        clear();
     return ret;
 }
 
@@ -1672,10 +1659,10 @@ bool core::no_lemmas_hold() const {
     return true;
 }
     
+    
 lbool core::test_check() {
-    vector<ineq> lits;
     lra.set_status(lp::lp_status::OPTIMAL);
-    return check(lits);
+    return check();
 }
 
 std::ostream& core::print_terms(std::ostream& out) const {
@@ -1826,162 +1813,13 @@ bool core::improve_bounds() {
     }
     return bounds_improved;
 }
-
-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 (!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::propagate() {
+    clear();
+    m_monomial_bounds.unit_propagate();
 }
 
-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;
-        }
-    }
+} // end of nla
 
-    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::propagate_monic_non_fixed_with_lemma(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;
-    }
-
-    void core::calculate_implied_bounds_for_monic(lp::lpvar monic_var) {
-        if (!is_monic_var(monic_var)) return;
-        m_propagated.reserve(monic_var + 1, false);
-        bool throttle = params().arith_nl_throttle_unit_prop();
-        if (throttle && m_propagated[monic_var])
-            return;
-        lpvar non_fixed, zero_var;
-        const auto& vars = m_emons[monic_var].vars();
-        if (!is_linear(vars, zero_var, non_fixed))
-            return;
-        if (throttle)    
-            trail().push(set_bitvector_trail(m_propagated, monic_var));    
-        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)
-                m_monomial_bounds.propagate_nonfixed(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() {
-        m_implied_bounds.clear();
-        m_improved_lower_bounds.reset();
-        m_improved_upper_bounds.reset();
-        m_column_types = &lra.get_column_types();
-        m_lemmas.clear();
-		// find m_monics_with_changed_bounds
-        for (lpvar j : lra.columns_with_changed_bounds()) {
-            if (is_monic_var(j))
-                m_monics_with_changed_bounds.insert(j);
-            else {
-                for (const auto & m: m_emons.get_use_list(j)) {
-                    m_monics_with_changed_bounds.insert(m.var());
-                }
-            }    
-        }
-    }
-}  // namespace nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 76397d529..5a597ae67 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -44,7 +44,6 @@ bool try_insert(const A& elem, B& collection) {
     return true;
 }
 
-
 class core {
     friend struct common;
     friend class new_lemma;
@@ -86,9 +85,10 @@ class core {
     smt_params_helper        m_params;
     std::function<bool(lpvar)> m_relevant;
     vector<lemma>            m_lemmas;
-    vector<ineq> *           m_literal_vec = nullptr;
+    vector<ineq>             m_literals;
+    vector<equality>         m_equalities;
+    vector<fixed_equality>   m_fixed_equalities;
     indexed_uint_set         m_to_refine;
-    indexed_uint_set         m_monics_with_changed_bounds;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -97,16 +97,13 @@ class core {
     divisions                m_divisions;
     intervals                m_intervals; 
     monomial_bounds          m_monomial_bounds;
-    
+    unsigned                 m_conflicts;
     horner                   m_horner;
     grobner                  m_grobner;
     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,17 +111,16 @@ class core {
     bool                     m_cautious_patching = true;
     lpvar                    m_patched_var = 0;
     monic const*             m_patched_monic = nullptr;      
-    bool_vector              m_propagated;
+
     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();
-    void clear_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
+
 public:    
     // constructor
-    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; }
+    core(lp::lar_solver& s, params_ref const& p, reslimit&);
+
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
     
@@ -314,7 +310,6 @@ public:
     bool sign_contradiction(const monic& m) const;
 
     bool var_is_fixed_to_zero(lpvar j) const;
-    bool fixed_var_has_big_bound(lpvar j) const;
     bool var_is_fixed_to_val(lpvar j, const rational& v) const;
 
     bool var_is_fixed(lpvar j) const;
@@ -392,11 +387,13 @@ public:
 
     bool  conflict_found() const;
     
-    lbool check(vector<ineq>& ineqs);
+    lbool check();
     lbool check_power(lpvar r, lpvar x, lpvar y);
     void check_bounded_divisions();
 
     bool  no_lemmas_hold() const;
+
+    void propagate();
     
     lbool  test_check();
     lpvar map_to_root(lpvar) const;
@@ -432,26 +429,22 @@ public:
     void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
+    vector<nla::lemma> const& lemmas() const { return m_lemmas; }
+    vector<nla::ineq> const& literals() const { return m_literals; }
+    vector<equality> const& equalities() const { return m_equalities; }
+    vector<fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
 
-    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_non_fixed_with_lemma(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;
-    vector<nla::lemma> const& lemmas() const { return m_lemmas; }        
-
+    void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
+    void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
 private:
-    lp::column_type get_column_type(unsigned j) const { return (*m_column_types)[j]; }
+    void restore_patched_values();
     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 53d8b0da6..f4d09810e 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -42,10 +42,14 @@ namespace nla {
     
     bool solver::need_check() { return m_core->has_relevant_monomial(); }
     
-    lbool solver::check(vector<ineq>& lits) {
-        return m_core->check(lits);
+    lbool solver::check() {
+        return m_core->check();
     }
 
+    void solver::propagate() {
+        m_core->propagate();
+    }
+    
     void solver::push(){
         m_core->push();
     }
@@ -54,8 +58,8 @@ namespace nla {
         m_core->pop(n);
     }
     
-    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)) {
+    solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit): 
+        m_core(alloc(core, s, p, limit)) {
     }
     
     bool solver::influences_nl_var(lpvar j) const {    
@@ -88,9 +92,6 @@ 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) {
         return m_core->check_power(r, x, y);
@@ -100,22 +101,20 @@ namespace nla {
         m_core->check_bounded_divisions();
     }
 
-    void solver::init_bound_propagation() {
-        m_core->init_bound_propagation();
-    }
-
     vector<nla::lemma> const& solver::lemmas() const {
         return m_core->lemmas();
     }
-
-    void solver::propagate_bounds_for_touched_monomials() {
-        init_bound_propagation();
-        for (unsigned v : m_core->monics_with_changed_bounds()) { 
-            calculate_implied_bounds_for_monic(v);
-            if (m_core->lra.get_status() == lp::lp_status::INFEASIBLE) {
-                break;
-            }
-        }
-        m_core->clear_monics_with_changed_bounds();        
+    
+    vector<nla::ineq> const& solver::literals() const {
+        return m_core->literals();
     }
+
+    vector<nla::equality> const& solver::equalities() const {
+        return m_core->equalities();
+    }
+
+    vector<nla::fixed_equality> const& solver::fixed_equalities() const {
+        return m_core->fixed_equalities();
+    }
+
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index acd724af9..fec27c32b 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -23,9 +23,10 @@ namespace nla {
     class solver {
         core* m_core;
     public:
-        
-        solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
+
+        solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
         ~solver();
+
         void add_monic(lpvar v, unsigned sz, lpvar const* vs);
         void add_idivision(lpvar q, lpvar x, lpvar y);
         void add_rdivision(lpvar q, lpvar x, lpvar y);
@@ -35,7 +36,7 @@ namespace nla {
         void push();
         void pop(unsigned scopes);
         bool need_check();
-        lbool check(vector<ineq>& lits);
+        lbool check();
         void propagate();
         lbool check_power(lpvar r, lpvar x, lpvar y);
         bool is_monic_var(lpvar) const;
@@ -46,9 +47,9 @@ 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();
-        vector<nla::lemma> const& lemmas() const;        
-        void propagate_bounds_for_touched_monomials();
+        vector<nla::lemma> const& lemmas() const;
+        vector<nla::ineq> const& literals() const;
+        vector<nla::fixed_equality> const& fixed_equalities() const;
+        vector<nla::equality> const& equalities() const;
     };
 }
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index 186c2e902..3930a62a9 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -24,6 +24,20 @@ namespace nla {
     typedef lp::explanation          expl_set;
     typedef lp::var_index            lpvar;
     const lpvar null_lpvar = UINT_MAX;
+
+    struct equality {
+        lp::lpvar i, j;
+        lp::explanation e;
+        equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {}
+    };
+    
+    struct fixed_equality {
+        lp::lpvar v;
+        rational       k;
+        lp::explanation e;
+        fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {}
+    };
+
     
     inline int rat_sign(const rational& r) { return r.is_pos()? 1 : ( r.is_neg()? -1 : 0); }
     inline rational rrat_sign(const rational& r) { return rational(rat_sign(r)); }
@@ -83,7 +97,6 @@ namespace nla {
         new_lemma& operator&=(const factorization& f);
         new_lemma& operator&=(lpvar j);
         new_lemma& operator|=(ineq const& i);
-        new_lemma& operator+=(ineq const& i);
         new_lemma& explain_fixed(lpvar j);
         new_lemma& explain_equiv(lpvar u, lpvar v);
         new_lemma& explain_var_separated_from_zero(lpvar j);
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 5893c8520..3174ad775 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_implied_bounds);
+            m_nla = alloc(nla::solver, *m_solver.get(), s().params(), m.limit());
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nla->push();
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 893fe4a43..17ab03ee6 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -253,7 +253,7 @@ namespace arith {
                 first = false;
                 reset_evidence();
                 m_explanation.clear();
-                be.explain_implied();                
+                lp().explain_implied_bound(be, m_bp);
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);
@@ -1416,7 +1416,7 @@ namespace arith {
     }
 
     void solver::assume_literals() {
-        for (auto const& ineq : m_nla_literals) {
+        for (auto const& ineq : m_nla->literals()) {
             auto lit = mk_ineq_literal(ineq);
             ctx.mark_relevant(lit);
             s().set_phase(lit);
@@ -1459,7 +1459,7 @@ namespace arith {
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals);
+        lbool r = m_nla->check();
         switch (r) {
         case l_false:
             assume_literals();
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 53b49a658..801eb474c 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -249,7 +249,6 @@ namespace arith {
 
         // lemmas
         lp::explanation     m_explanation;
-        vector<nla::ineq>   m_nla_literals;
         literal_vector      m_core, m_core2;
         vector<rational>    m_coeffs;
         svector<enode_pair> m_eqs;
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index a538b2a80..42cda4bfb 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -501,8 +501,9 @@ namespace euf {
         for (expr* arg : clause)
             std::cout << "\n " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
+        std::cout.flush();
 
-        if (is_rup(proof_hint)) 
+        if (false && is_rup(proof_hint)) 
             diagnose_rup_failure(clause);
             
         add_clause(clause);
@@ -527,9 +528,6 @@ namespace euf {
             for (expr* f : core)
                 std::cout << mk_pp(f, m) << "\n";
         }
-        SASSERT(false);
-        
-        exit(0);
     }
 
     void smt_proof_checker::collect_statistics(statistics& st) const {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index fca7fcacf..9fcda7f64 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -71,8 +71,6 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
                           ('arith.nl.grobner_frequency', UINT, 4, 'grobner\'s call frequency'),
                           ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'),
-                          ('arith.nl.use_lemmas_in_unit_prop', BOOL, False, 'use lemmas in monomial unit propagation'),
-                          ('arith.nl.throttle_unit_prop', BOOL, True, 'unit propogate a monomial only once per scope'),
                           ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
                           ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),
                           ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 777961334..bf27777c4 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -90,14 +90,14 @@ namespace smt {
         return proof_ref(m);
     }
 
-    void clause_proof::add(clause& c) {
+    void clause_proof::add(clause& c, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         justification* j = c.get_justification();
         auto st = kind2st(c.get_kind());
         auto pr = justification2proof(st, j);
         CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-        update(c, st, pr);        
+        update(c, st, pr, simp_lits);        
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
@@ -137,12 +137,15 @@ namespace smt {
         update(st, m_lits, pr);
     }
 
-    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
+    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit1));
         m_lits.push_back(ctx.literal2expr(lit2));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         auto st = kind2st(k);
         auto pr = justification2proof(st, j);
         update(st, m_lits, pr);
@@ -160,7 +163,7 @@ namespace smt {
     }
 
     void clause_proof::del(clause& c) {
-        update(c, status::deleted, justification2proof(status::deleted, nullptr));
+        update(c, status::deleted, justification2proof(status::deleted, nullptr), nullptr);
     }
 
     std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
@@ -190,7 +193,9 @@ namespace smt {
         if (ctx.get_fparams().m_clause_proof)
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
-            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());        
+            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
+        static unsigned s_count = 0;
+        
         if (m_has_log) {
             init_pp_out();
             auto& out = *m_pp_out;
@@ -220,12 +225,15 @@ namespace smt {
         }
     }
 
-    void clause_proof::update(clause& c, status st, proof* p) {
+    void clause_proof::update(clause& c, status st, proof* p, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         for (literal lit : c) 
-            m_lits.push_back(ctx.literal2expr(lit));        
+            m_lits.push_back(ctx.literal2expr(lit));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         update(st, m_lits, p);        
     }
 
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index 1c5931136..d7cc421cf 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -68,7 +68,7 @@ namespace smt {
         void init_pp_out();
         
         void update(status st, expr_ref_vector& v, proof* p);
-        void update(clause& c, status st, proof* p);
+        void update(clause& c, status st, proof* p, literal_buffer const* simp_lits);
         status kind2st(clause_kind k);
         proof_ref justification2proof(status st, justification* j);
         void log(status st, proof* p);
@@ -79,8 +79,8 @@ namespace smt {
         clause_proof(context& ctx);
         void shrink(clause& c, unsigned new_size);
         void add(literal lit, clause_kind k, justification* j);
-        void add(literal lit1, literal lit2, clause_kind k, justification* j);
-        void add(clause& c);
+        void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr);
+        void add(clause& c, literal_buffer const* simp_lits = nullptr);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
         void propagate(literal lit, justification const& j, literal_vector const& ante);
         void del(clause& c);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index d075c0652..2561fbb5a 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -601,6 +601,7 @@ namespace smt {
 
         finalize_resolve(conflict, not_l);
 
+
         return true;
     }
 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0e9e39996..b6d1e2f2b 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1378,12 +1378,12 @@ namespace smt {
     clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) {
         TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
         m_clause_proof.add(num_lits, lits, k, j);
+        literal_buffer simp_lits;
         switch (k) {
         case CLS_TH_AXIOM:
             dump_axiom(num_lits, lits);
             Z3_fallthrough;
         case CLS_AUX: {
-            literal_buffer simp_lits;
             if (m_searching)
                 dump_lemma(num_lits, lits);
             if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
@@ -1451,7 +1451,7 @@ namespace smt {
                 else if (get_assignment(l2) == l_false) {
                     assign(l1, b_justification(~l2));
                 }
-                m_clause_proof.add(l1, l2, k, j);
+                m_clause_proof.add(l1, l2, k, j, &simp_lits);
                 m_stats.m_num_mk_bin_clause++;
                 return nullptr;
             }
@@ -1464,7 +1464,7 @@ namespace smt {
             bool reinit         = save_atoms;
             SASSERT(!lemma || j == 0 || !j->in_region());
             clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.data());
-            m_clause_proof.add(*cls);
+            m_clause_proof.add(*cls, &simp_lits);
             if (lemma) {
                 cls->set_activity(activity);
                 if (k == CLS_LEARNED) {
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index dd9ba2dfe..470ea5f7b 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1535,7 +1535,8 @@ namespace smt {
         m_stats.m_max_min++;
         unsigned best_efforts = 0;
         bool inc = false;
-        
+
+
         SASSERT(!maintain_integrality || valid_assignment());
         SASSERT(satisfy_bounds());
 
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index ae0af89ec..0a2b6e938 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -765,10 +765,8 @@ typename theory_arith<Ext>::numeral theory_arith<Ext>::get_monomial_fixed_var_pr
 template<typename Ext>
 expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
     SASSERT(is_pure_monomial(m));
-    for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-        expr * arg = to_app(m)->get_arg(i);
-        theory_var _var = expr2var(arg);
-        if (!is_fixed(_var))
+    for (expr* arg : *to_app(m)) {
+        if (!is_fixed(expr2var(arg)))
             return arg;
     }
     return nullptr;
@@ -780,7 +778,7 @@ expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
-    TRACE("non_linear", tout << "checking whether v" << v << " became linear...\n";);
+    TRACE("non_linear_verbose", tout << "checking whether v" << v << " became linear...\n";);
     if (m_data[v].m_nl_propagated)
         return false; // already propagated this monomial.
     expr * m = var2expr(v);
@@ -819,6 +817,11 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
             ctx.mark_as_relevant(rhs);
         }
         TRACE("non_linear_bug", tout << "enode: " << ctx.get_enode(rhs) << " enode_id: " << ctx.get_enode(rhs)->get_owner_id() << "\n";);
+        IF_VERBOSE(3,
+                   for (auto* arg : *to_app(m)) 
+                       if (is_fixed(expr2var(arg)))
+                           verbose_stream() << mk_pp(arg, get_manager()) << " = " << -k << "\n");
+            
         theory_var new_v = expr2var(rhs);
         SASSERT(new_v != null_theory_var);
         new_lower    = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
@@ -906,7 +909,7 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
         return false;
     if (!reflection_enabled())
         return false;
-    TRACE("non_linear", tout << "propagating linear monomials...\n";);
+    TRACE("non_linear_verbose", tout << "propagating linear monomials...\n";);
     bool p = false;
     // CMW: m_nl_monomials can grow during this loop, so
     // don't use iterators.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2a7412c29..a5c5084ab 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_implied_bounds);
+            m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nla->push();
@@ -1528,14 +1528,12 @@ public:
         unsigned old_sz = m_assume_eq_candidates.size();
         unsigned num_candidates = 0;
         int start = ctx().get_random_value();
-        unsigned num_relevant = 0;
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
             if (!th.is_relevant_and_shared(n1)) {                    
                 continue;
             }
-            ++num_relevant;
             ensure_column(v);
             if (!is_registered_var(v))
                 continue;
@@ -1553,7 +1551,7 @@ public:
                 num_candidates++;
             }
         }
-
+            
         if (num_candidates > 0) {
             ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
         }
@@ -1605,8 +1603,7 @@ public:
         case l_true:
             return FC_DONE;
         case l_false:
-            for (const nla::lemma & l : m_nla->lemmas()) 
-                false_case_of_check_nla(l);
+            add_lemmas();
             return FC_CONTINUE;
         case l_undef:
             return FC_GIVEUP;
@@ -1803,8 +1800,7 @@ public:
         if (!m_nla)
             return true;
         m_nla->check_bounded_divisions();
-        for (auto & lemma : m_nla->lemmas())
-            false_case_of_check_nla(lemma);
+        add_lemmas();
         return m_nla->lemmas().empty();
     }
 
@@ -2003,7 +1999,7 @@ public:
             // create term >= 0 (or term <= 0)
             atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
         return literal(ctx().get_bool_var(atom), pos);
-    }
+    }    
 
     void false_case_of_check_nla(const nla::lemma & l) {
         m_lemma = l; //todo avoid the copy
@@ -2024,14 +2020,11 @@ public:
     
     final_check_status check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_nla->check(m_nla_literals);
+        lbool r = m_nla->check();
 
         switch (r) {
         case l_false:
-            for (const nla::ineq& i : m_nla_literals)
-                assume_literal(i); 
-            for (const nla::lemma & l : m_nla->lemmas()) 
-                false_case_of_check_nla(l);
+            add_lemmas();
             return FC_CONTINUE;
         case l_true:
             return assume_eqs()? FC_CONTINUE: FC_DONE;
@@ -2120,6 +2113,8 @@ public:
     bool propagate_core() {
         m_model_is_initialized = false;
         flush_bound_axioms();
+        // disabled in master:
+        propagate_nla(); 
         if (!can_propagate_core())
             return false;
         m_new_def = false;        
@@ -2151,7 +2146,6 @@ public:
             break;
         case l_true:
             propagate_basic_bounds();
-            propagate_bounds_with_nlp();            
             propagate_bounds_with_lp_solver();
             break;
         case l_undef:
@@ -2161,6 +2155,47 @@ public:
         return true;            
     }
 
+    void propagate_nla() {
+        if (m_nla) {
+            m_nla->propagate();
+            add_lemmas();
+            add_equalities();
+        }
+    }
+
+    void add_equalities() {
+        if (!propagate_eqs()) 
+            return;
+        for (auto const& [v,k,e] : m_nla->fixed_equalities())
+            add_equality(v, k, e);
+        for (auto const& [i,j,e] : m_nla->equalities())
+            add_eq(i,j,e,false);
+    }
+
+    void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
+        //verbose_stream() << "equality " << j << " " << k << "\n";
+        TRACE("arith", tout << "equality " << j << " " << k << "\n");
+        theory_var v;
+        if (k == 1)
+            v = m_one_var;
+        else if (k == 0)
+            v = m_zero_var;
+        else if (!m_value2var.find(k, v))
+            return;
+        theory_var w = lp().local_to_external(j);
+        if (w < 0)
+            return;
+        lpvar i = register_theory_var_in_lar_solver(v);
+        add_eq(i, j, exp, true);
+    }
+
+    void add_lemmas() {
+        for (const nla::ineq& i : m_nla->literals())
+            assume_literal(i); 
+        for (const nla::lemma & l : m_nla->lemmas()) 
+            false_case_of_check_nla(l);
+    }
+
     bool should_propagate() const {
         return bound_prop_mode::BP_NONE != propagation_mode();
     }
@@ -2173,50 +2208,33 @@ public:
         set_evidence(j, m_core, m_eqs);
         m_explanation.add_pair(j, v);
     }
+    
+    void propagate_bounds_with_lp_solver() {
+        if (!should_propagate()) 
+            return;
+
+        m_bp.init();
+        lp().propagate_bounds_for_touched_rows(m_bp);
+
+        if (!m.inc()) 
+            return;
 
-    void finish_bound_propagation() {
         if (is_infeasible()) {
             get_infeasibility_explanation_and_set_conflict();
             // verbose_stream() << "unsat\n";
         }
         else {
-            for (auto &ib : m_bp.ibounds()) {
+            unsigned count = 0, prop = 0;
+            for (auto& ib : m_bp.ibounds()) {
                 m.inc();
                 if (ctx().inconsistent())
                     break;
-                propagate_lp_solver_bound(ib);
+                ++prop;
+                count += propagate_lp_solver_bound(ib);
             }
         }
     }
 
-    void propagate_bounds_with_lp_solver() {
-        if (!should_propagate()) 
-            return;
-        m_bp.init();
-        lp().propagate_bounds_for_touched_rows(m_bp);
-
-        if (m.inc()) 
-            finish_bound_propagation();
-    }
-    
-    void propagate_bounds_for_monomials() {
-        m_nla->propagate_bounds_for_touched_monomials();
-        for (const auto & l : m_nla->lemmas()) 
-            false_case_of_check_nla(l);
-    }
-
-    void propagate_bounds_with_nlp() {
-        if (!m_nla)
-            return;
-        if (is_infeasible() || !should_propagate())
-            return;
-
-        propagate_bounds_for_monomials();
-
-        if (m.inc())
-            finish_bound_propagation();
-    }
-
     bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
         theory_var v = lp().local_to_external(vi);
         if (v == null_theory_var) 
@@ -3161,8 +3179,7 @@ public:
         std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
         scoped_trace_stream _sts(th, fn);
 
-       
-        // SASSERT(validate_eq(x, y));
+        //VERIFY(validate_eq(x, y));
         ctx().assign_eq(x, y, eq_justification(js));
     }
     
@@ -3206,12 +3223,11 @@ public:
     }
  
     lp::explanation     m_explanation;
-    vector<nla::ineq>       m_nla_literals;
     literal_vector      m_core;
     svector<enode_pair> m_eqs;
     vector<parameter>   m_params;
 
-        void reset_evidence() {
+    void reset_evidence() {
         m_core.reset();
         m_eqs.reset();
         m_params.reset();
@@ -3278,6 +3294,7 @@ public:
               display(tout << "is-conflict: " << is_conflict << "\n"););
         for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
+
         
         // SASSERT(validate_conflict(m_core, m_eqs));
         if (is_conflict) {
@@ -3533,6 +3550,8 @@ public:
         lbool r = nctx.check();
         if (r == l_true) {
             nctx.display_asserted_formulas(std::cout);
+            std::cout.flush();
+            std::cout.flush();
         }
         return l_true != r;
     }
@@ -3882,6 +3901,7 @@ public:
                 IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n"); 
         }
     }
+
 };
     
 theory_lra::theory_lra(context& ctx):