From 5bda42e104122377efb8d9c1e7a54c726e31cf9d Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 25 Jun 2025 06:04:07 -0700
Subject: [PATCH] rename new_lemma to lemma_builder

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/monomial_bounds.cpp     | 14 +++++-----
 src/math/lp/nla_basics_lemmas.cpp   | 32 +++++++++++-----------
 src/math/lp/nla_basics_lemmas.h     |  4 +--
 src/math/lp/nla_core.cpp            | 42 ++++++++++++++---------------
 src/math/lp/nla_core.h              | 14 +++++-----
 src/math/lp/nla_divisions.cpp       | 10 +++----
 src/math/lp/nla_grobner.cpp         | 12 ++++-----
 src/math/lp/nla_grobner.h           |  2 +-
 src/math/lp/nla_intervals.cpp       |  2 +-
 src/math/lp/nla_monotone_lemmas.cpp |  4 +--
 src/math/lp/nla_order_lemmas.cpp    | 39 +++++++++++++++++++--------
 src/math/lp/nla_order_lemmas.h      | 14 +++++-----
 src/math/lp/nla_powers.cpp          | 18 ++++++-------
 src/math/lp/nla_tangent_lemmas.cpp  |  8 +++---
 src/math/lp/nla_types.h             | 30 ++++++++++-----------
 src/math/lp/nra_solver.cpp          |  4 +--
 src/params/smt_params_helper.pyg    |  1 +
 17 files changed, 135 insertions(+), 115 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index cf78fa3dd..66505c698 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -110,7 +110,7 @@ namespace nla {
             dep.get_upper_dep(range, ex);
             if (is_too_big(upper))
                 return false;
-            new_lemma lemma(c(), "propagate value - upper bound of range is below value");
+            lemma_builder lemma(c(), "propagate value - upper bound of range is below value");
             lemma &= ex;
             lemma |= ineq(v, cmp, upper); 
             TRACE(nla_solver, dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";);
@@ -124,7 +124,7 @@ namespace nla {
             dep.get_lower_dep(range, ex);
             if (is_too_big(lower))
                 return false;
-            new_lemma lemma(c(), "propagate value - lower bound of range is above value");
+            lemma_builder lemma(c(), "propagate value - lower bound of range is above value");
             lemma &= ex;
             lemma |= ineq(v, cmp, lower); 
             TRACE(nla_solver, dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";);
@@ -196,7 +196,7 @@ namespace nla {
             // p even, range.upper < 0, v^p >= 0 -> infeasible
             if (p % 2 == 0 && rational(dep.upper(range)).is_neg()) {
                 ++c().lra.settings().stats().m_nla_propagate_bounds;
-                new_lemma lemma(c(), "range requires a non-negative upper bound");
+                lemma_builder lemma(c(), "range requires a non-negative upper bound");
                 lemma &= ex;
                 return true;
             }
@@ -208,7 +208,7 @@ namespace nla {
                 if ((p % 2 == 1) || c().val(v).is_pos()) {
                     ++c().lra.settings().stats().m_nla_propagate_bounds;
                     auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
-                    new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
+                    lemma_builder lemma(c(), "propagate value - root case - upper bound of range is below value");
                     lemma &= ex;
                     lemma |= ineq(v, le, r);
                     return true;
@@ -218,7 +218,7 @@ namespace nla {
                     ++c().lra.settings().stats().m_nla_propagate_bounds;
                     SASSERT(!r.is_neg());
                     auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
-                    new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
+                    lemma_builder lemma(c(), "propagate value - root case - upper bound of range is below negative value");
                     lemma &= ex;
                     lemma |= ineq(v, ge, -r);
                     return true;
@@ -242,7 +242,7 @@ namespace nla {
                 auto le = dep.lower_is_open(range) ? llc::LT : llc::LE;
                 lp::explanation ex;
                 dep.get_lower_dep(range, ex);
-                new_lemma lemma(c(), "propagate value - root case - lower bound of range is above value");
+                lemma_builder lemma(c(), "propagate value - root case - lower bound of range is above value");
                 lemma &= ex;
                 lemma |= ineq(v, ge, r);
                 if (p % 2 == 0)
@@ -380,7 +380,7 @@ namespace nla {
             return false;
         lp::explanation exp;
         c().lra.get_infeasibility_explanation(exp);
-        new_lemma lemma(c(), "propagate fixed - infeasible lra");
+        lemma_builder lemma(c(), "propagate fixed - infeasible lra");
         lemma &= exp;
         return true;
     }
diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 5a480ec16..20d6cde75 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -83,7 +83,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monic& m, int product_si
         TRACE(nla_solver_bl, tout << "zero product sign: " << pp_mon(_(), m)<< "\n";);
         generate_zero_lemmas(m);
     } else {
-        new_lemma lemma(c(), __FUNCTION__);
+        lemma_builder lemma(c(), __FUNCTION__);
         for (lpvar j: m.vars()) {
             negate_strict_sign(lemma, j);
         }
@@ -149,7 +149,7 @@ bool basics::basic_sign_lemma(bool derived) {
 // the value of the i-th monic has to be equal to the value of the k-th monic modulo sign
 // but it is not the case in the model
 void basics::generate_sign_lemma(const monic& m, const monic& n, const rational& sign) {
-    new_lemma lemma(c(), "sign lemma");
+    lemma_builder lemma(c(), "sign lemma");
     TRACE(nla_solver,
           tout << "m = " << pp_mon_with_vars(_(), m);
           tout << "n = " << pp_mon_with_vars(_(), n);
@@ -175,7 +175,7 @@ lpvar basics::find_best_zero(const monic& m, unsigned_vector & fixed_zeros) cons
 }
 
 void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) {
-    new_lemma lemma(c(), "x = 0 => x*y = 0");
+    lemma_builder lemma(c(), "x = 0 => x*y = 0");
     lemma |= ineq(zero_j,  llc::NE, 0);
     lemma |= ineq(m.var(), llc::EQ, 0);
 }
@@ -183,7 +183,7 @@ void basics::add_trivial_zero_lemma(lpvar zero_j, const monic& m) {
 void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj) {
     TRACE(nla_solver_bl, tout << "sign_of_zj = " << sign_of_zj << "\n";);
     // we know all the signs
-    new_lemma lemma(c(), "strict case 0");
+    lemma_builder lemma(c(), "strict case 0");
     lemma |= ineq(zero_j, sign_of_zj == 1? llc::GT : llc::LT, 0);
     for (unsigned j : m.vars()) {
         if (j != zero_j) {
@@ -194,12 +194,12 @@ void basics::generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, in
 }
 
 void basics::add_fixed_zero_lemma(const monic& m, lpvar j) {
-    new_lemma lemma(c(), "fixed zero");
+    lemma_builder lemma(c(), "fixed zero");
     lemma.explain_fixed(j);
     lemma |= ineq(m.var(), llc::EQ, 0);
 }
 
-void basics::negate_strict_sign(new_lemma& lemma, lpvar j) {
+void basics::negate_strict_sign(lemma_builder& lemma, lpvar j) {
     TRACE(nla_solver_details, tout << pp_var(c(), j) << " " << val(j).is_zero() << "\n";);
     if (!val(j).is_zero()) {
         int sign = nla::rat_sign(val(j));
@@ -226,7 +226,7 @@ bool basics::basic_lemma_for_mon_zero(const monic& rm, const factorization& f) {
             return false;
     }
     TRACE(nla_solver, c().trace_print_monic_and_factorization(rm, f, tout););
-    new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0");
+    lemma_builder lemma(c(), "xy = 0 -> x = 0 or y = 0");
     lemma.explain_fixed(var(rm));
     std::unordered_set<lpvar> processed;
     for (auto j : f) {
@@ -298,7 +298,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const monic& rm, const factori
     for (auto fc : f) {
         if (!c().var_is_fixed_to_zero(var(fc))) 
             continue;
-        new_lemma lemma(c(), "x = 0 or y = 0 -> xy = 0");
+        lemma_builder lemma(c(), "x = 0 or y = 0 -> xy = 0");
         lemma.explain_fixed(var(fc));
         lemma.explain_var_separated_from_zero(var(rm));
         lemma &= rm;
@@ -345,7 +345,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
 
     //    (mon_var != 0 || u != 0) & mon_var = +/- u =>
     //    v = 1 or v = -1
-    new_lemma lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
+    lemma_builder lemma(c(), "|xa| = |x| & x != 0 -> |a| = 1");
     lemma.explain_var_separated_from_zero(mon_var_is_sep_from_zero ? mon_var : u);    
     lemma.explain_equiv(mon_var, u);        
     lemma |= ineq(v, llc::EQ, 1);        
@@ -387,7 +387,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization&
 */
 void basics::generate_pl_on_mon(const monic& m, unsigned k) {
     SASSERT(!c().has_real(m));
-    new_lemma lemma(c(), "generate_pl_on_mon");
+    lemma_builder lemma(c(), "generate_pl_on_mon");
     unsigned mon_var = m.var();
     rational mv = val(mon_var);
     SASSERT(abs(mv) < abs(val(m.vars()[k])));
@@ -423,7 +423,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
         generate_pl_on_mon(m, factor_index);
         return;
     }
-    new_lemma lemma(c(), "generate_pl");
+    lemma_builder lemma(c(), "generate_pl");
     int fi = 0;
     rational mv = var_val(m);
     rational sm = rational(nla::rat_sign(mv));
@@ -459,7 +459,7 @@ bool basics::is_separated_from_zero(const factorization& f) const {
 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {        
     TRACE(nla_solver,  c().trace_print_monic_and_factorization(rm, f, tout););
     SASSERT(var_val(rm).is_zero() && !c().rm_check(rm));
-    new_lemma lemma(c(), "xy = 0 -> x = 0 or y = 0");
+    lemma_builder lemma(c(), "xy = 0 -> x = 0 or y = 0");
     if (!is_separated_from_zero(f)) {
         lemma |= ineq(var(rm), llc::NE, 0);
         for (auto j : f) {
@@ -511,7 +511,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
     if (!can_create_lemma_for_mon_neutral_from_factors_to_monic_model_based(m, m, not_one, sign))
         return false;
        
-    new_lemma lemma(c(), __FUNCTION__);
+    lemma_builder lemma(c(), __FUNCTION__);
     for (auto j : m.vars()) {
         if (not_one != j) 
             lemma |= ineq(j, llc::NE, val(j));
@@ -556,7 +556,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based(const monic
     // v = 1
     // v = -1
 
-    new_lemma lemma(c(), __FUNCTION__);
+    lemma_builder lemma(c(), __FUNCTION__);
     lemma |= ineq(mon_var, llc::EQ, 0);        
     lemma |= ineq(term(u, rational(val(u) == -val(mon_var) ? 1 : -1), mon_var), llc::NE, 0);
     lemma |= ineq(v, llc::EQ, 1);
@@ -641,7 +641,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
             return false;
     TRACE(nla_solver_bl, tout << "not_one = " << not_one << "\n";);
         
-    new_lemma lemma(c(), __FUNCTION__);
+    lemma_builder lemma(c(), __FUNCTION__);
 
     for (auto j : f) {
         lpvar var_j = var(j);
@@ -665,7 +665,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based(const monic& rm, const fac
     TRACE(nla_solver_bl, c().trace_print_monic_and_factorization(rm, f, tout););
     for (auto j : f) {
         if (val(j).is_zero()) {
-            new_lemma lemma(c(), "x = 0 => x*... = 0");
+            lemma_builder lemma(c(), "x = 0 => x*... = 0");
             lemma |= ineq(var(j), llc::NE, 0);
             lemma |= ineq(f.mon().var(), llc::EQ, 0);
             lemma &= f;
diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h
index 58fb0e92f..812491d04 100644
--- a/src/math/lp/nla_basics_lemmas.h
+++ b/src/math/lp/nla_basics_lemmas.h
@@ -14,7 +14,7 @@
 
 namespace nla {
 class core;
-class new_lemma;
+class lemma_builder;
 struct basics: common {
     basics(core *core);
     bool basic_sign_lemma_on_two_monics(const monic& m, const monic& n);
@@ -84,7 +84,7 @@ struct basics: common {
     void generate_strict_case_zero_lemma(const monic& m, unsigned zero_j, int sign_of_zj);
     
     void add_fixed_zero_lemma(const monic& m, lpvar j);
-    void negate_strict_sign(new_lemma& lemma, lpvar j);
+    void negate_strict_sign(lemma_builder& lemma, lpvar j);
     // x != 0 or y = 0 => |xy| >= |y|
     void proportion_lemma_model_based(const monic& rm, const factorization& factorization);
     // if there are no zero factors then |m| >= |m[factor_index]|
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 6acc2b043..08027558f 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -350,7 +350,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun
 }
     
 // return true iff the negation of the ineq can be derived from the constraints
-bool core::explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs) {
+bool core::explain_ineq(lemma_builder& lemma, const lp::lar_term& t, llc cmp, const rational& rs) {
     // check that we have something like 0 < 0, which is always false and can be safely
     // removed from the lemma
         
@@ -410,7 +410,7 @@ bool core::explain_by_equiv(const lp::lar_term& t, lp::explanation& e) const {
     return true;            
 }
 
-void core::mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs) {
+void core::mk_ineq_no_expl_check(lemma_builder& lemma, lp::lar_term& t, llc cmp, const rational& rs) {
     TRACE(nla_solver_details, lra.print_term_as_indices(t, tout << "t = "););
     lemma |= ineq(cmp, t, rs);
     CTRACE(nla_solver, ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
@@ -429,7 +429,7 @@ llc apply_minus(llc cmp) {
 }   
     
 // the monics should be equal by modulo sign but this is not so in the model
-void core::fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign) {
+void core::fill_explanation_and_lemma_sign(lemma_builder& lemma, const monic& a, const monic & b, rational const& sign) {
     SASSERT(sign == 1 || sign == -1);
     lemma &= a;
     lemma &= b;
@@ -899,7 +899,7 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const {
 }
 
 
-void core::negate_factor_equality(new_lemma& lemma, const factor& c,
+void core::negate_factor_equality(lemma_builder& lemma, const factor& c,
                                   const factor& d) {
     if (c == d)
         return;
@@ -910,7 +910,7 @@ void core::negate_factor_equality(new_lemma& lemma, const factor& c,
     lemma |= ineq(term(i, rational(iv == jv ? -1 : 1), j), llc::NE, 0);    
 }
     
-void core::negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
+void core::negate_factor_relation(lemma_builder& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b) {
     rational a_fs = sign_to_rat(canonize_sign(a));
     rational b_fs = sign_to_rat(canonize_sign(b));
     llc cmp = a_sign*val(a) < b_sign*val(b)? llc::GE : llc::LE;
@@ -1040,11 +1040,11 @@ rational core::val(const factorization& f) const {
     return r;
 }
 
-new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
+lemma_builder::lemma_builder(core& c, char const* name):name(name), c(c) {
     c.m_lemmas.push_back(lemma());
 }
 
-new_lemma& new_lemma::operator|=(ineq const& ineq) {
+lemma_builder& lemma_builder::operator|=(ineq const& ineq) {
     if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
         CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
         SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq));
@@ -1054,7 +1054,7 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
 }
     
 
-new_lemma::~new_lemma() {
+lemma_builder::~lemma_builder() {
     static int i = 0;
     (void)i;
     (void)name;
@@ -1067,22 +1067,22 @@ new_lemma::~new_lemma() {
     TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
 }
 
-lemma& new_lemma::current() const {
+lemma& lemma_builder::current() const {
     return c.m_lemmas.back();
 }
 
-new_lemma& new_lemma::operator&=(lp::explanation const& e) {
+lemma_builder& lemma_builder::operator&=(lp::explanation const& e) {
     expl().add_expl(e);
     return *this;
 }
 
-new_lemma& new_lemma::operator&=(const monic& m) {
+lemma_builder& lemma_builder::operator&=(const monic& m) {
     for (lpvar j : m.vars())
         *this &= j;
     return *this;
 }
 
-new_lemma& new_lemma::operator&=(const factor& f) {
+lemma_builder& lemma_builder::operator&=(const factor& f) {
     if (f.type() == factor_type::VAR) 
         *this &= f.var();
     else 
@@ -1090,7 +1090,7 @@ new_lemma& new_lemma::operator&=(const factor& f) {
     return *this;
 }
 
-new_lemma& new_lemma::operator&=(const factorization& f) {
+lemma_builder& lemma_builder::operator&=(const factorization& f) {
     if (f.is_mon())
         return *this;
     for (const auto& fc : f) {
@@ -1099,19 +1099,19 @@ new_lemma& new_lemma::operator&=(const factorization& f) {
     return *this;
 }
 
-new_lemma& new_lemma::operator&=(lpvar j) {
+lemma_builder& lemma_builder::operator&=(lpvar j) {
     c.m_evars.explain(j, expl());
     return *this;
 }
 
-new_lemma& new_lemma::explain_fixed(lpvar j) {
+lemma_builder& lemma_builder::explain_fixed(lpvar j) {
     SASSERT(c.var_is_fixed(j));
     explain_existing_lower_bound(j);
     explain_existing_upper_bound(j);
     return *this;
 }
 
-new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) {
+lemma_builder& lemma_builder::explain_equiv(lpvar a, lpvar b) {
     SASSERT(abs(c.val(a)) == abs(c.val(b)));
     if (c.vars_are_equiv(a, b)) {
         *this &= a;
@@ -1123,7 +1123,7 @@ new_lemma& new_lemma::explain_equiv(lpvar a, lpvar b) {
     return *this;
 }
 
-new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) {
+lemma_builder& lemma_builder::explain_var_separated_from_zero(lpvar j) {
     SASSERT(c.var_is_separated_from_zero(j));
     if (c.lra.column_has_upper_bound(j) && 
         (c.lra.get_upper_bound(j)< lp::zero_of_type<lp::impq>())) 
@@ -1133,7 +1133,7 @@ new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) {
     return *this;
 }
 
-new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
+lemma_builder& lemma_builder::explain_existing_lower_bound(lpvar j) {
     SASSERT(c.has_lower_bound(j));
     lp::explanation ex;
     c.lra.push_explanation(c.lra.get_column_lower_bound_witness(j), ex);
@@ -1142,7 +1142,7 @@ new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
     return *this;
 }
 
-new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
+lemma_builder& lemma_builder::explain_existing_upper_bound(lpvar j) {
     SASSERT(c.has_upper_bound(j));
     lp::explanation ex;
     c.lra.push_explanation(c.lra.get_column_upper_bound_witness(j), ex);
@@ -1150,7 +1150,7 @@ new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
     return *this;
 }
     
-std::ostream& new_lemma::display(std::ostream & out) const {
+std::ostream& lemma_builder::display(std::ostream & out) const {
     auto const& lemma = current();
 
     for (auto p : lemma.expl()) {
@@ -1175,7 +1175,7 @@ std::ostream& new_lemma::display(std::ostream & out) const {
     return out;
 }
     
-void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
+void core::negate_relation(lemma_builder& lemma, unsigned j, const rational& a) {
     SASSERT(val(j) != a);
     lemma |= ineq(j, val(j) < a ? llc::GE : llc::LE, a);   
 }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 955adeb07..46526b6a0 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -46,7 +46,7 @@ bool try_insert(const A& elem, B& collection) {
 
 class core {
     friend struct common;
-    friend class new_lemma;
+    friend class lemma_builder;
     friend class grobner;
     friend class order;
     friend struct basics;
@@ -263,7 +263,7 @@ public:
                         std::ostream& out);
 
         
-    void mk_ineq_no_expl_check(new_lemma& lemma, lp::lar_term& t, llc cmp, const rational& rs);
+    void mk_ineq_no_expl_check(lemma_builder& lemma, lp::lar_term& t, llc cmp, const rational& rs);
     
     void maybe_add_a_factor(lpvar i,
                             const factor& c,
@@ -273,7 +273,7 @@ public:
 
     llc apply_minus(llc cmp);
     
-    void fill_explanation_and_lemma_sign(new_lemma& lemma, const monic& a, const monic & b, rational const& sign);
+    void fill_explanation_and_lemma_sign(lemma_builder& lemma, const monic& a, const monic & b, rational const& sign);
 
     svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
 
@@ -319,7 +319,7 @@ public:
     bool var_is_separated_from_zero(lpvar j) const;
 
     bool vars_are_equiv(lpvar a, lpvar b) const;    
-    bool explain_ineq(new_lemma& lemma, const lp::lar_term& t, llc cmp, const rational& rs);
+    bool explain_ineq(lemma_builder& lemma, const lp::lar_term& t, llc cmp, const rational& rs);
     bool explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const;
     bool explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const;
     bool explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const;
@@ -370,9 +370,9 @@ public:
     bool rm_check(const monic&) const;
     std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
 
-    void negate_relation(new_lemma& lemma, unsigned j, const rational& a);
-    void negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d);    
-    void negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
+    void negate_relation(lemma_builder& lemma, unsigned j, const rational& a);
+    void negate_factor_equality(lemma_builder& lemma, const factor& c, const factor& d);    
+    void negate_factor_relation(lemma_builder& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
 
     bool  find_bfc_to_refine_on_monic(const monic&, factorization & bf);
     
diff --git a/src/math/lp/nla_divisions.cpp b/src/math/lp/nla_divisions.cpp
index 72b6d73f0..49b4ee765 100644
--- a/src/math/lp/nla_divisions.cpp
+++ b/src/math/lp/nla_divisions.cpp
@@ -55,7 +55,7 @@ namespace nla {
         auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
             auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
                 if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) {
-                    new_lemma lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2");
+                    lemma_builder lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2");
                     lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
                     lemma |= ineq(y2, llc::LE, 0);
                     lemma |= ineq(x1, llc::LT, 0);
@@ -69,7 +69,7 @@ namespace nla {
         auto monotonicity2 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
             auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
                 if (y2val <= y1val && y1val < 0 && x1val >= x2val && x2val >= 0 && q1val > q2val) {
-                    new_lemma lemma(c, "y2 <= y1 < 0 & x1 >= x2 >= 0 => x1/y1 <= x2/y2");
+                    lemma_builder lemma(c, "y2 <= y1 < 0 & x1 >= x2 >= 0 => x1/y1 <= x2/y2");
                     lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
                     lemma |= ineq(y1, llc::GE, 0);
                     lemma |= ineq(term(x1, rational(-1), x2), llc::LT, 0);
@@ -83,7 +83,7 @@ namespace nla {
         auto monotonicity3 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
             auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
                 if (y2val <= y1val && y1val < 0 && x1val <= x2val && x2val <= 0 && q1val < q2val) {
-                    new_lemma lemma(c, "y2 <= y1 < 0 & x1 <= x2 <= 0 => x1/y1 >= x2/y2");
+                    lemma_builder lemma(c, "y2 <= y1 < 0 & x1 <= x2 <= 0 => x1/y1 >= x2/y2");
                     lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
                     lemma |= ineq(y1, llc::GE, 0);
                     lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0);
@@ -187,14 +187,14 @@ namespace nla {
             rational hi = yv * div_v + yv - 1;
             rational lo = yv * div_v;
             if (xv > hi) {
-                new_lemma lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)");
+                lemma_builder lemma(c, "y = yv & x <= yv * div(xv, yv) + yv - 1 => div(p, y) <= div(xv, yv)");
                 lemma |= ineq(y, llc::NE, yv); 
                 lemma |= ineq(x, llc::GT, hi); 
                 lemma |= ineq(q, llc::LE, div_v);  
                 return;
             }
             if (xv < lo) {
-                new_lemma lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)");
+                lemma_builder lemma(c, "y = yv & x >= yv * div(xv, yv) => div(xv, yv) <= div(x, y)");
                 lemma |= ineq(y, llc::NE, yv);
                 lemma |= ineq(x, llc::LT, lo);
                 lemma |= ineq(q, llc::GE, div_v);
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 9f5abb51a..09660a2a6 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -142,7 +142,7 @@ namespace nla {
             ineq new_eq(v, llc::EQ, rational::zero());
             if (c().ineq_holds(new_eq))
                 return false;
-            new_lemma lemma(c(), "pdd-eq");
+            lemma_builder lemma(c(), "pdd-eq");
             add_dependencies(lemma, eq);
             lemma |= new_eq;
             return true;
@@ -159,7 +159,7 @@ namespace nla {
             ineq new_eq(term(a, v), llc::EQ, b);
             if (c().ineq_holds(new_eq))
                 return false;
-            new_lemma lemma(c(), "pdd-eq");
+            lemma_builder lemma(c(), "pdd-eq");
             add_dependencies(lemma, eq);
             lemma |= new_eq;
             return true;
@@ -202,7 +202,7 @@ namespace nla {
             if (c().ineq_holds(i))
                 return false;
 
-        new_lemma lemma(c(), "pdd-factored");
+        lemma_builder lemma(c(), "pdd-factored");
         add_dependencies(lemma, eq);
         for (auto const& i : ineqs)
             lemma |= i;
@@ -219,7 +219,7 @@ namespace nla {
     }
 
 
-    void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
+    void grobner::add_dependencies(lemma_builder& lemma, const dd::solver::equation& eq) {
         lp::explanation exp;
         explain(eq, exp);
         lemma &= exp;
@@ -344,7 +344,7 @@ namespace nla {
         }
         evali.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);  
         std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
-            new_lemma lemma(m_core, "pdd");
+            lemma_builder lemma(m_core, "pdd");
             lemma &= e;
         };
         if (di.check_interval_for_conflict_on_zero(i_wd, e.dep(), f)) {
@@ -686,7 +686,7 @@ namespace nla {
 
     bool grobner::add_nla_conflict(const dd::solver::equation& eq) {
         if (is_nla_conflict(eq)) {
-            new_lemma lemma(m_core,"nla-conflict");
+            lemma_builder lemma(m_core,"nla-conflict");
             lp::explanation exp;
             explain(eq, exp);
             lemma &= exp;
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 4ce0593fa..ee41e4dae 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -44,7 +44,7 @@ namespace nla {
         bool propagate_linear_equations();
         bool propagate_linear_equations(dd::solver::equation const& eq);
         
-        void add_dependencies(new_lemma& lemma, dd::solver::equation const& eq);
+        void add_dependencies(lemma_builder& lemma, dd::solver::equation const& eq);
         void explain(dd::solver::equation const& eq, lp::explanation& exp);
 
         bool add_horner_conflict(dd::solver::equation const& eq);
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 27fb8b2ce..b0edb256b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -89,7 +89,7 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
     m_core->lp_settings().stats().m_cross_nested_forms++;
     scoped_dep_interval i(get_dep_intervals());
     std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
-        new_lemma lemma(*m_core, "check_nex");
+        lemma_builder lemma(*m_core, "check_nex");
         lemma &= e;
     };
     if (!interval_of_expr<e_with_deps::without_deps>(n, 1, i, f)) {
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index cc9241446..e09d1717e 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -54,7 +54,7 @@ void monotone::monotonicity_lemma(monic const& m) {
     
 */
 void monotone::monotonicity_lemma_gt(const monic& m) {
-    new_lemma lemma(c(), "monotonicity > ");
+    lemma_builder lemma(c(), "monotonicity > ");
     rational product(1);
     for (lpvar j : m.vars()) {
         auto v = c().val(j);
@@ -76,7 +76,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) {
     x <= -2 & y >= 3 => x*y <= -6
 */
 void monotone::monotonicity_lemma_lt(const monic& m) {
-    new_lemma lemma(c(), "monotonicity <");
+    lemma_builder lemma(c(), "monotonicity <");
     rational product(1);
     for (lpvar j : m.vars()) {
         auto v = c().val(j);
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 494681c91..159a02a5d 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -10,6 +10,7 @@
 #include "math/lp/nla_core.h"
 #include "math/lp/nla_common.h"
 #include "math/lp/factorization_factory_imp.h"
+#include "util/trail.h"
 
 namespace nla {
 
@@ -83,17 +84,33 @@ void order::order_lemma_on_binomial(const monic& ac) {
 void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
     if (!c().var_is_int(x) && val(x).is_big())
         return;
-    if (&xy == m_last_binom)
-        return;
-    c().trail().push(value_trail(m_last_binom, &xy));
+    // throttle!!!
+
     SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(val(y));
-    new_lemma lemma(c(), __FUNCTION__);
+    lemma_builder lemma(c(), __FUNCTION__);
     lemma |= ineq(y,                                   sy == 1      ? llc::LE : llc::GE, 0); // negate sy
     lemma |= ineq(x,                                   sy*sign == 1 ? llc::GT : llc::LT , val(x)); 
     lemma |= ineq(term(xy.var(), - val(x), y), sign == 1    ? llc::LE : llc::GE, 0);
 }
 
+bool order::throttle_monic(const monic& ac, std::string const & debug_location ) { // todo - remove debug location!
+    // Check if throttling is enabled
+    if (!c().params().arith_nl_thrl())
+        return false;
+    
+    // Check if this monic has already been processed using its variable ID
+    if (m_processed_monics.contains(ac.var())) {
+        TRACE(nla_solver, tout << "throttled at " << debug_location << "\n";);
+        return true;
+    }
+    
+    // Mark this monic as processed and add to trail for backtracking
+    m_processed_monics.insert(ac.var());
+    c().trail().push(insert_map(m_processed_monics, ac.var()));
+    return false;
+}
+
 // We look for monics e = m.rvars()[k]*d and see if we can create an order lemma for m and  e
 void order::order_lemma_on_factor_binomial_explore(const monic& ac, bool k) {
     TRACE(nla_solver, tout << "ac = " <<  pp_mon_with_vars(c(), ac););
@@ -170,7 +187,7 @@ void order::generate_mon_ol(const monic& ac,
     SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
     SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
     
-    new_lemma lemma(_(), __FUNCTION__);
+    lemma_builder lemma(_(), __FUNCTION__);
     lemma |= ineq(term(c_sign, c), llc::LE, 0);
     lemma &= c; // this explains c == +- d
     lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0);
@@ -220,7 +237,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
     if (mv != fv && !c().has_real(m)) {            
         bool gt = mv > fv;
         for (unsigned j = 0, k = 1; j < 2; j++, k--) {
-            new_lemma lemma(_(), __FUNCTION__);
+            lemma_builder lemma(_(), __FUNCTION__);
             order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt);
             lemma &= ab;
             lemma &= m;
@@ -255,7 +272,7 @@ void order::generate_ol_eq(const monic& ac,
                         const monic& bc,
                         const factor& b) {
     
-    new_lemma lemma(_(), __FUNCTION__);
+    lemma_builder lemma(_(), __FUNCTION__);
     IF_VERBOSE(100, 
                verbose_stream() 
                << var_val(ac) << "(" << mul_val(ac) << "): " << ac 
@@ -280,7 +297,7 @@ void order::generate_ol(const monic& ac,
                         const monic& bc,
                         const factor& b) {
     
-    new_lemma lemma(_(), __FUNCTION__);
+    lemma_builder lemma(_(), __FUNCTION__);
     TRACE(nla_solver, _().trace_print_ol(ac, a, c, bc, b, tout););        
     IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac 
                << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
@@ -335,7 +352,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
    given: sign * m = ab
    lemma b != val(b) || sign*m <= a*val(b)
 */
-void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
+void order::order_lemma_on_ab_gt(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
     SASSERT(sign * var_val(m) > val(a) * val(b));
     // negate b == val(b)
     lemma |= ineq(b, llc::NE, val(b));
@@ -346,7 +363,7 @@ void order::order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rationa
    given: sign * m = ab
    lemma b != val(b) || sign*m >= a*val(b)
 */
-void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
+void order::order_lemma_on_ab_lt(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b) {
     TRACE(nla_solver, tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) <<
           ", b = "; c().print_var(b, tout) << "\n";);
     SASSERT(sign * var_val(m) < val(a) * val(b));
@@ -356,7 +373,7 @@ void order::order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rationa
     lemma |= ineq(term(sign, m.var(), -val(b), a), llc::GE, 0);
 }
 
-void order::order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) {
+void order::order_lemma_on_ab(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt) {
     if (gt)
         order_lemma_on_ab_gt(lemma, m, sign, a, b);
     else 
diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h
index d53e5317c..dba858c82 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -9,17 +9,19 @@
 #pragma once
 #include "math/lp/factorization.h"
 #include "math/lp/nla_common.h"
+#include "util/hashtable.h"
+#include "util/hash.h"
 
 namespace nla {
 class core;
-class new_lemma;
+class lemma_builder;
 class order: common {
 public:
     order(core *c) : common(c) {}
     void order_lemma();
     
-    monic const* m_last_binom = nullptr;
-
+    int_hashtable<int_hash, default_eq<int>> m_processed_monics;
+    bool throttle_monic(const monic&, const std::string & debug_location);
    private:
 
     bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,
@@ -41,9 +43,9 @@ public:
     void order_lemma_on_factorization(const monic& rm, const factorization& ab);
     
 
-    void order_lemma_on_ab_gt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b);
-    void order_lemma_on_ab_lt(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b);
-    void order_lemma_on_ab(new_lemma& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt);
+    void order_lemma_on_ab_gt(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b);
+    void order_lemma_on_ab_lt(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b);
+    void order_lemma_on_ab(lemma_builder& lemma, const monic& m, const rational& sign, lpvar a, lpvar b, bool gt);
     void order_lemma_on_factor_binomial_explore(const monic& m, bool k);
     void order_lemma_on_factor_binomial_rm(const monic& ac, bool k, const monic& bd);
     void order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic& bd, const factor& b, lpvar d);
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index b934ad16a..038d26fff 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -89,7 +89,7 @@ namespace nla {
         lemmas.reset();
 
         auto x_exp_0 = [&]() {
-            new_lemma lemma(c, "x != 0 => x^0 = 1");
+            lemma_builder lemma(c, "x != 0 => x^0 = 1");
             lemma |= ineq(x, llc::EQ, rational::zero());
             lemma |= ineq(y, llc::NE, rational::zero());
             lemma |= ineq(r, llc::EQ, rational::one());
@@ -97,7 +97,7 @@ namespace nla {
         };
 
         auto zero_exp_y = [&]() {
-            new_lemma lemma(c, "y != 0 => 0^y = 0");
+            lemma_builder lemma(c, "y != 0 => 0^y = 0");
             lemma |= ineq(x, llc::NE, rational::zero());
             lemma |= ineq(y, llc::EQ, rational::zero());
             lemma |= ineq(r, llc::EQ, rational::zero());
@@ -105,14 +105,14 @@ namespace nla {
         };
 
         auto x_gt_0 = [&]() {
-            new_lemma lemma(c, "x > 0 => x^y > 0");
+            lemma_builder lemma(c, "x > 0 => x^y > 0");
             lemma |= ineq(x, llc::LE, rational::zero());
             lemma |= ineq(r, llc::GT, rational::zero());
             return l_false;
         };
 
         auto y_lt_1 = [&]() {
-            new_lemma lemma(c, "x > 1, y < 0 => x^y < 1");
+            lemma_builder lemma(c, "x > 1, y < 0 => x^y < 1");
             lemma |= ineq(x, llc::LE, rational::one());
             lemma |= ineq(y, llc::GE, rational::zero());
             lemma |= ineq(r, llc::LT, rational::one());
@@ -120,7 +120,7 @@ namespace nla {
         };
 
         auto y_gt_1 = [&]() {
-            new_lemma lemma(c, "x > 1, y > 0 => x^y > 1");
+            lemma_builder lemma(c, "x > 1, y > 0 => x^y > 1");
             lemma |= ineq(x, llc::LE, rational::one());
             lemma |= ineq(y, llc::LE, rational::zero());
             lemma |= ineq(r, llc::GT, rational::one());
@@ -128,7 +128,7 @@ namespace nla {
         };
 
         auto x_ge_3 = [&]() {
-            new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
+            lemma_builder lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
             lemma |= ineq(x, llc::LT, rational(3));
             lemma |= ineq(y, llc::EQ, rational::zero());
             lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one());
@@ -172,21 +172,21 @@ namespace nla {
                 if (rval == r2val)
                     return l_true;
                 if (c.random() % 2 == 0) {
-                    new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0");
+                    lemma_builder lemma(c, "x == x0, y == y0 => r = x0^y0");
                     lemma |= ineq(x, llc::NE, xval);
                     lemma |= ineq(y, llc::NE, yval);
                     lemma |= ineq(r, llc::EQ, r2val);
                     return l_false;
                 }
                 if (yval > 0 && r2val > rval) {
-                    new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
+                    lemma_builder lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
                     lemma |= ineq(x, llc::LT, xval);
                     lemma |= ineq(y, llc::LT, yval);
                     lemma |= ineq(r, llc::GE, r2val);
                     return l_false;
                 }
                 if (r2val < rval) {
-                    new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
+                    lemma_builder lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
                     lemma |= ineq(x, llc::LE, rational::zero());
                     lemma |= ineq(x, llc::GT, xval);
                     lemma |= ineq(y, llc::GT, yval);
diff --git a/src/math/lp/nla_tangent_lemmas.cpp b/src/math/lp/nla_tangent_lemmas.cpp
index ff4b6f93c..512b54cc2 100644
--- a/src/math/lp/nla_tangent_lemmas.cpp
+++ b/src/math/lp/nla_tangent_lemmas.cpp
@@ -61,7 +61,7 @@ private:
 
     core & c() { return m_tang.c(); }
 
-    void explain(new_lemma& lemma) {
+    void explain(lemma_builder& lemma) {
         if (!m_is_mon) {
             lemma &= m_m;
             lemma &= m_x;
@@ -70,7 +70,7 @@ private:
     }
 
     void generate_plane(const point & pl) {
-        new_lemma lemma(c(), "generate tangent plane");
+        lemma_builder lemma(c(), "generate tangent plane");
         c().negate_relation(lemma, m_jx, m_x.rat_sign()*pl.x);
         c().negate_relation(lemma, m_jy, m_y.rat_sign()*pl.y);
 #if Z3DEBUG
@@ -91,7 +91,7 @@ private:
     }
 
     void generate_line1() {
-        new_lemma lemma(c(), "tangent line 1");
+        lemma_builder lemma(c(), "tangent line 1");
         // Should be  v = val(m_x)*val(m_y), and val(factor) = factor.rat_sign()*var(factor.var())
         lemma |= ineq(m_jx, llc::NE, c().val(m_jx));
         lemma |= ineq(lp::lar_term(m_j,  - m_y.rat_sign() * m_xy.x,  m_jy), llc::EQ, 0);
@@ -99,7 +99,7 @@ private:
     }
 
     void generate_line2() {            
-        new_lemma lemma(c(), "tangent line 2");
+        lemma_builder lemma(c(), "tangent line 2");
         lemma |= ineq(m_jy, llc::NE, c().val(m_jy));
         lemma |= ineq(lp::lar_term(m_j, - m_x.rat_sign() * m_xy.y, m_jx), llc::EQ, 0);
         explain(lemma);
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index f0f796652..2f061559d 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -69,27 +69,27 @@ namespace nla {
     // all constraints are assumed added to the lemma
     // correctness of the lemma can be checked at this point.
     //
-    class new_lemma {
+    class lemma_builder {
         char const* name;
         core& c;
         lemma& current() const;
         
     public:
-        new_lemma(core& c, char const* name);
-        ~new_lemma();
+        lemma_builder(core& c, char const* name);
+        ~lemma_builder();
         lemma& operator()() { return current(); }
         std::ostream& display(std::ostream& out) const;
-        new_lemma& operator&=(lp::explanation const& e);
-        new_lemma& operator&=(const monic& m);
-        new_lemma& operator&=(const factor& f);
-        new_lemma& operator&=(const factorization& f);
-        new_lemma& operator&=(lpvar j);
-        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);
-        new_lemma& explain_existing_lower_bound(lpvar j);
-        new_lemma& explain_existing_upper_bound(lpvar j);    
+        lemma_builder& operator&=(lp::explanation const& e);
+        lemma_builder& operator&=(const monic& m);
+        lemma_builder& operator&=(const factor& f);
+        lemma_builder& operator&=(const factorization& f);
+        lemma_builder& operator&=(lpvar j);
+        lemma_builder& operator|=(ineq const& i);
+        lemma_builder& explain_fixed(lpvar j);
+        lemma_builder& explain_equiv(lpvar u, lpvar v);
+        lemma_builder& explain_var_separated_from_zero(lpvar j);
+        lemma_builder& explain_existing_lower_bound(lpvar j);
+        lemma_builder& explain_existing_upper_bound(lpvar j);    
         
         lp::explanation& expl() { return current().expl(); }
         
@@ -97,7 +97,7 @@ namespace nla {
     };
 
 
-    inline std::ostream& operator<<(std::ostream& out, new_lemma const& l) {
+    inline std::ostream& operator<<(std::ostream& out, lemma_builder const& l) {
         return l.display(out);
     }
 
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 5603c4aed..bc498f9e4 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -228,7 +228,7 @@ struct solver::imp {
                 ex.push_back(idx);
                 TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";);
             }
-            nla::new_lemma lemma(m_nla_core, __FUNCTION__);
+            nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
             lemma &= ex;
             m_nla_core.set_use_nra_model(true);
             break;
@@ -416,7 +416,7 @@ struct solver::imp {
                 dm.linearize(static_cast<u_dependency*>(c), lv);
             for (auto ci : lv)
                 ex.push_back(ci);
-            nla::new_lemma lemma(m_nla_core, __FUNCTION__);
+            nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
             lemma &= ex;
             break;
         }
diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index c1eb0148a..8e1124ee7 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -65,6 +65,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.order', BOOL, True, 'run order lemmas'),
                           ('arith.nl.expp', BOOL, False, 'expensive patching'),
                           ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'),
+                          ('arith.nl.thrl', BOOL, True, 'throttle repeated lemmas - debug, remove later!!!'),
                           ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'),
                           ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
                           ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'),