diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index 999444b3b..fcae2e5da 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -63,9 +63,10 @@ public:
             return ret;                
         }
     }
-
-    bool separated_from_zero(pdd const& p, u_dependency*& dep) {
-        return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep);
+	// f meant to be called when the separation happens
+    template <typename T>
+    bool separated_from_zero(pdd const& p, u_dependency*& dep, std::function<void (const T)>& f) {
+        return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep, f);
     }
 
 };
diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp
index 3381f9440..adb93beef 100644
--- a/src/math/interval/dep_intervals.cpp
+++ b/src/math/interval/dep_intervals.cpp
@@ -86,28 +86,6 @@ bool dep_intervals::separated_from_zero_on_upper(const interval& i) const {
     return true;
 }
 
-bool dep_intervals::check_interval_for_conflict_on_zero(const interval & i, u_dependency*& dep) {
-    return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep);
-}
-
-bool dep_intervals::check_interval_for_conflict_on_zero_upper(const interval & i, u_dependency*& dep) {
-    if (!separated_from_zero_on_upper(i))
-        return false;
-    TRACE("dep_intervals", display(tout, i););
-    dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
-    return true;
-}
-
-bool dep_intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency*& dep) {
-    if (!separated_from_zero_on_lower(i)) {
-        return false;
-    }
-    TRACE("dep_intervals", display(tout, i););
-    dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
-    return true;
-}
-
-
 std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const {
     if (m_imanager.lower_is_inf(i)) {
         out << "(-oo";
diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index d0c0343be..fd82b4dc7 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -255,15 +255,44 @@ public:
     inline bool separated_from_zero(const interval& i) const {
         return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i);
     }
-    bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*&);
-    bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*&);
-    bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*&);
+    template <typename T> 
+    bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
+        return check_interval_for_conflict_on_zero_lower(i, dep, f) || check_interval_for_conflict_on_zero_upper(i, dep, f);
+    }
+    template <typename T> 
+    bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
+        if (!separated_from_zero_on_lower(i)) {
+            return false;
+        }
+        TRACE("dep_intervals", display(tout, i););
+        dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
+        T expl;
+        linearize(dep, expl);
+        f(expl);
+        return true;
+    }
+    template <typename T> 
+    bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
+        if (!separated_from_zero_on_upper(i))
+            return false;
+        TRACE("dep_intervals", display(tout, i););
+        dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
+        T expl;
+        linearize(dep, expl);
+        f(expl);
+        return true;
+    }
     mpq const& lower(interval const& a) const { return m_config.lower(a); }
     mpq const& upper(interval const& a) const { return m_config.upper(a); }
     bool is_empty(interval const& a) const;
     void set_interval_for_scalar(interval&, const rational&);
     template <typename T> 
-    void linearize(u_dependency* dep, T& expl) const { m_dep_manager.linearize(dep, expl); }
+    void linearize(u_dependency* dep, T& expl) const {
+        vector<unsigned, false> v;
+        m_dep_manager.linearize(dep, v);
+        for (unsigned ci: v)
+            expl.push_back(ci);
+    }
 
     void reset() { m_dep_manager.reset(); }
     
diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h
index 1ed7a5947..c122f9f2b 100644
--- a/src/math/lp/explanation.h
+++ b/src/math/lp/explanation.h
@@ -41,6 +41,9 @@ public:
         m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
     }
 
+    void push_back(constraint_index j) {
+        push_justification(j);
+    }
     
     void add(const explanation& e) { for (auto j: e.m_set_of_ci) add(j); }
     template <typename T>
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 0bc500fc4..90be43350 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1284,9 +1284,11 @@ lbool core::incremental_linearization(bool constraint_derived) {
 lbool core::inner_check(bool constraint_derived) {
     if (constraint_derived) {
         if (need_to_call_algebraic_methods())
-            if (m_horner.horner_lemmas()) {
-                switch( m_nla_settings.run_grobner()) {                    
-                case nla_settings::BOTH_GROBNER:
+            if (!m_horner.horner_lemmas()) {
+                clear_and_resize_active_var_set();
+                find_nl_cluster();
+                switch(m_nla_settings.run_grobner()) {                    
+                case nla_settings::NEX_AND_BDD_GROBNER:
                     init_nex_grobner(m_nex_grobner.get_nex_creator());
                     m_nex_grobner.grobner_lemmas();
                     run_pdd_grobner();
@@ -1410,6 +1412,16 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
 
 void core::run_pdd_grobner() {
     m_pdd_manager.resize(m_lar_solver.number_of_vars());
+    for (unsigned i : m_rows) {
+        add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
+    }
+    m_pdd_grobner.saturate();
+    for (auto eq : m_pdd_grobner.equations()) {
+        check_pdd_eq(eq);
+    }
+}
+
+void core::check_pdd_eq(const dd::grobner::equation* e) {
     NOT_IMPLEMENTED_YET();
 }
 
@@ -1442,7 +1454,12 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
     }            
 }
 
-void core::find_nl_cluster(nex_creator& nc) {
+void core::add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row) {
+    NOT_IMPLEMENTED_YET();
+}
+
+
+void core::find_nl_cluster() {
     prepare_rows_and_active_vars();
     svector<lpvar> q;
     for (lpvar j : m_to_refine) {        
@@ -1455,7 +1472,6 @@ void core::find_nl_cluster(nex_creator& nc) {
         q.pop_back();
         add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
     }
-    set_active_vars_weights(nc);
     TRACE("grobner", display_matrix_of_m_rows(tout););
 }
 
@@ -1498,9 +1514,8 @@ void core::display_matrix_of_m_rows(std::ostream & out) const {
 }
 
 void core::init_nex_grobner(nex_creator & nc) {   
-    find_nl_cluster(nc);
-    clear_and_resize_active_var_set();
     TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";);
+    set_active_vars_weights(nc);
     for (unsigned i : m_rows) {
         m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]);
     }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 9aeb66151..bfb26742b 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -391,7 +391,7 @@ public:
     std::ostream& print_terms(std::ostream&) const;
     std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
     void run_pdd_grobner();
-    void find_nl_cluster(nex_creator&);
+    void find_nl_cluster();
     void prepare_rows_and_active_vars();
     void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  svector<lpvar>& q);
     void init_nex_grobner(nex_creator&);
@@ -399,6 +399,8 @@ public:
     void display_matrix_of_m_rows(std::ostream & out) const;
     void set_active_vars_weights(nex_creator&);
     var_weight get_var_weight(lpvar) const;
+    void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);    
+    void check_pdd_eq(const dd::grobner::equation*);
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index d5aa9f05b..e2e0eae1e 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -79,7 +79,11 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
     }
     auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
     TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
-    m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps);
+    std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
+                                                         m_core->add_empty_lemma();
+                                                         m_core->current_expl().add(e);
+                                                     };
+    m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps, f);
     m_dep_intervals.reset(); // clean the memory allocated by the interval bound dependencies
     return true;
 }
diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h
index a3e01d4c9..700d1cf9a 100644
--- a/src/math/lp/nla_settings.h
+++ b/src/math/lp/nla_settings.h
@@ -23,7 +23,7 @@ namespace nla {
 class nla_settings {
 public:
     enum run_grobner_enum {
-                           NO_GROBNER, NEX_GROBNER, PDD_GROBNER, BOTH_GROBNER };
+                           NO_GROBNER, NEX_GROBNER, PDD_GROBNER, NEX_AND_BDD_GROBNER };
 private:
     bool     m_run_order;
     bool     m_run_tangents;