diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 3ff33a879..f99f640bf 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -169,8 +169,8 @@ public:
         return params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_horner_frequency() == 0; 
     }
 
-    bool need_run_grobner() const { 
-        return params().arith_nl_grobner() && lp_settings().stats().m_nla_calls % params().arith_nl_grobner_frequency() == 0; 
+    bool need_run_grobner() const {
+        return params().arith_nl_grobner();         
     }
 
     void set_active_vars_weights(nex_creator&);
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index a7c7dd762..b3ad6173e 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -13,7 +13,6 @@ Author:
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
-#include "math/lp/nex.h"
 #include "math/grobner/pdd_solver.h"
 #include "math/dd/pdd_interval.h"
 #include "math/dd/pdd_eval.h"
@@ -33,17 +32,33 @@ namespace nla {
     }
 
     void grobner::operator()() {
+
+        if (lra.column_count() > 5000)
+            return;
+
         if (m_quota == 0)
             m_quota = c().params().arith_nl_gr_q();                    
 
-        if (m_quota == 1)
+        if (m_quota == 1) {
+            m_delay_base++;
+            m_delay = m_delay_base;
+            m_quota = c().params().arith_nl_gr_q();
+        }
+
+        if (m_delay > 0) {
+            --m_delay;
             return;
+        }
+        
 
         lp_settings().stats().m_grobner_calls++;
         find_nl_cluster();        
         configure();
         m_solver.saturate();
 
+        if (m_delay_base > 0)
+            --m_delay_base;
+        
         if (is_conflicting())
             return;
 
@@ -56,6 +71,9 @@ namespace nla {
 
             if (propagate_factorization())
                 return;
+
+            if (false && propagate_linear_equations())
+                return;
         }
         catch (...) {
             
@@ -63,15 +81,14 @@ namespace nla {
 
         // DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e););
 
-
+        ++m_delay_base;
         if (m_quota > 0)
            --m_quota;
 
-        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
+        IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
         IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
 
 
-
 #if 0
         // diagnostics: did we miss something
         vector<dd::pdd> eqs;
@@ -82,18 +99,16 @@ namespace nla {
     }
 
     bool grobner::is_conflicting() {
-        unsigned conflicts = 0;
-        for (auto eq : m_solver.equations()) 
-            if (is_conflicting(*eq) && ++conflicts >= m_solver.number_of_conflicts_to_report())
-                break;
-
-        if (conflicts > 0) 
-            lp_settings().stats().m_grobner_conflicts++;
-
-        TRACE("grobner", m_solver.display(tout));
-        IF_VERBOSE(2, if (conflicts > 0) verbose_stream() << "grobner conflict\n");
-
-        return conflicts > 0;
+        bool is_conflict = false;
+        for (auto eq : m_solver.equations()) {
+            if (is_conflicting(*eq)) {
+                lp_settings().stats().m_grobner_conflicts++;
+                TRACE("grobner", m_solver.display(tout));
+                IF_VERBOSE(3, verbose_stream() << "grobner conflict\n");
+                return true;
+            }
+        }
+        return false;
     }
 
     bool grobner::propagate_bounds() {
@@ -293,22 +308,29 @@ namespace nla {
         return out;
     }
 
-    bool grobner::is_conflicting(const dd::solver::equation& e) {
-        for (auto j : e.poly().free_vars()) 
-            if (lra.column_is_free(j))
-                return false;
+    bool grobner::equation_is_true(dd::solver::equation const& eq) {
+        if (any_of(eq.poly().free_vars(), [&](unsigned j) { return lra.column_is_free(j); }))
+            return true;
+        dd::pdd_eval eval;
+        eval.var2val() = [&](unsigned j){ return val(j); };
+        return eval(eq.poly()) == 0;
+    }
+    
 
+    bool grobner::is_conflicting(const dd::solver::equation& e) {
+        if (equation_is_true(e))
+            return false;
         auto& di = c().m_intervals.get_dep_intervals();
-        dd::pdd_interval eval(di);
-        eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
+        dd::pdd_interval evali(di);
+        evali.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
             if (deps) c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
             else c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
         };
         scoped_dep_interval i(di), i_wd(di);
-        eval.get_interval<dd::w_dep::without_deps>(e.poly(), i);    
+        evali.get_interval<dd::w_dep::without_deps>(e.poly(), i);    
         if (!di.separated_from_zero(i)) {
             TRACE("grobner", m_solver.display(tout << "not separated from 0 ", e) << "\n";
-                  eval.get_interval_distributed<dd::w_dep::without_deps>(e.poly(), i);
+                  evali.get_interval_distributed<dd::w_dep::without_deps>(e.poly(), i);
                   tout << "separated from 0: " << di.separated_from_zero(i) << "\n";
                   for (auto j : e.poly().free_vars()) {
                       scoped_dep_interval a(di);
@@ -316,14 +338,17 @@ namespace nla {
                       c().m_intervals.display(tout << "j" << j << " ", a); tout << " ";
                   }
                   tout << "\n");
+
             
+            if (add_horner_conflict(e))
+                return true;
 #if 0
             if (add_nla_conflict(e)) 
                 return true;
 #endif
             return false;
         }
-        eval.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);  
+        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 &= e;
@@ -356,6 +381,57 @@ namespace nla {
         return false;
     }
 
+    bool grobner::propagate_linear_equations() {
+        unsigned changed = 0;
+        for (auto eq : m_solver.equations()) 
+            if (propagate_linear_equations(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
+                return true;
+        return changed > 0;
+    }
+    
+    bool grobner::propagate_linear_equations(dd::solver::equation const& e) {
+        if (equation_is_true(e))
+            return false;
+        if (!e.poly().is_linear())
+            return false;
+
+        rational lc(1);
+        for (auto const& [coeff, vars] : e.poly())
+            lc = lcm(denominator(coeff), lc);
+        auto q = e.poly();
+
+        
+#if 0
+        // TODO: instead add a row to lra solver, make sure that make_feasible
+        // gets invoked (for example, bail out of final check).
+        vector<std::pair<lp::mpq, unsigned>> coeffs;        
+        while (!q.is_val()) {
+            coeffs.push_back({lc*q.hi().val(), q.var()});
+            q = q.lo();
+        }
+
+        lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
+        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, -lc*q.val(), e.dep());
+
+#else
+        
+        new_lemma lemma(m_core,"nla-linear");
+        lp::explanation exp;
+        explain(e, exp);
+        lemma &= exp;
+        term t;
+        while (!q.is_val()) {
+            t.add_monomial(lc*q.hi().val(), q.var());
+            q = q.lo();
+        }
+        lemma |= ineq(t, llc::EQ, -lc*q.val());
+#endif
+        
+        return true;
+    }
+
+
     void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
         if (c().active_var_set_contains(j))
             return;
@@ -581,6 +657,50 @@ namespace nla {
         return l_false == c().m_nra.check(eqs);
     }
 
+    bool grobner::add_horner_conflict(const dd::solver::equation& eq) {
+        nex_creator& nc = m_nex_creator;
+        nc.pop(0);
+        nex_creator::sum_factory sum(nc);
+        unsigned row_index = 0;
+        u_map<nex_var*> var2nex;
+        for (auto v : eq.poly().free_vars()) 
+            var2nex.insert(v, nc.mk_var(v));
+        unsigned mx = 0;
+        for (auto v : eq.poly().free_vars())
+            mx = std::max(v, mx);
+        nc.set_number_of_vars(mx + 1);
+        for (auto const& [coeff, vars] : eq.poly()) {
+            switch (vars.size()) {
+            case 0:
+                sum += nc.mk_scalar(coeff);
+                break;
+            case 1:
+                sum += nc.mk_mul(coeff, var2nex[vars[0]]);
+                break;
+            default:
+                nc.m_mk_mul.reset();
+                nc.m_mk_mul *= coeff;
+                for (auto v : vars)
+                    nc.m_mk_mul *= var2nex[v];
+                sum += nc.m_mk_mul.mk();
+                break;
+            }
+        }
+        nex* e = nc.simplify(sum.mk());
+        if (e->get_degree() < 2 || !e->is_sum())
+            return false;
+
+        auto dep = eq.dep();
+        cross_nested cn(
+            [this, dep](const nex* n) { bool r = c().m_intervals.check_nex(n, dep); TRACE("grobner", tout << "check " << r << " " << *n << "\n"); return r; },
+            [this](unsigned j)   { return c().var_is_fixed(j); },
+            [this]() { return c().random(); }, nc);
+        cn.run(to_sum(e));
+        bool ret = cn.done();
+        TRACE("grobner", tout << "Horner " << ret << " " << eq.poly() << "\n");
+        return ret;
+    }
+
     bool grobner::add_nla_conflict(const dd::solver::equation& eq) {
         if (is_nla_conflict(eq)) {
             new_lemma lemma(m_core,"nla-conflict");
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 40fbb1ffc..dc5a188a5 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -24,28 +24,37 @@ namespace nla {
         lp::lar_solver&          lra;
         indexed_uint_set         m_rows;
         unsigned                 m_quota = 0;
+        unsigned                 m_delay_base = 0;
+        unsigned                 m_delay = 0;
 
         lp::lp_settings& lp_settings();
 
         // solving
         bool is_conflicting();
-        bool is_conflicting(const dd::solver::equation& eq);
+        bool is_conflicting(dd::solver::equation const& eq);
 
         bool propagate_bounds();
-        bool propagate_bounds(const dd::solver::equation& eq);
+        bool propagate_bounds(dd::solver::equation const& eq);
 
         bool propagate_eqs();
-        bool propagate_fixed(const dd::solver::equation& eq);
+        bool propagate_fixed(dd::solver::equation const& eq);
 
         bool propagate_factorization();
-        bool propagate_factorization(const dd::solver::equation& eq);
-                
-        void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
-        void explain(const dd::solver::equation& eq, lp::explanation& exp);
+        bool propagate_factorization(dd::solver::equation const& eq);
 
-        bool is_nla_conflict(const dd::solver::equation& eq);
-        bool add_nla_conflict(const dd::solver::equation& eq);
-        void check_missing_propagation(const dd::solver::equation& eq);
+
+        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 explain(dd::solver::equation const& eq, lp::explanation& exp);
+
+        bool add_horner_conflict(dd::solver::equation const& eq);
+        bool is_nla_conflict(dd::solver::equation const& eq);
+        bool add_nla_conflict(dd::solver::equation const& eq);
+        void check_missing_propagation(dd::solver::equation const& eq);
+
+        bool equation_is_true(dd::solver::equation const& eq);
 
         // setup
         void configure();