diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index c661ee4ef..a72f5ec5f 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -799,6 +799,7 @@ namespace dd {
         st.update("superposed", m_stats.m_superposed);
         st.update("degree", m_stats.m_max_expr_degree);
         st.update("size", m_stats.m_max_expr_size);
+        st.update("conflicts", m_stats.m_conflicts);
     }
             
     std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index 262e82329..4c2f9168e 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -37,6 +37,7 @@ public:
         unsigned m_max_expr_degree;
         unsigned m_superposed;
         unsigned m_compute_steps;
+        unsigned m_conflicts;
         void reset() { memset(this, 0, sizeof(*this)); }
         stats() { reset(); }
     };
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index cf96fe90f..1689b7008 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1450,6 +1450,7 @@ void core::check_pdd_eq(const dd::grobner::equation* e) {
                                                          current_expl().add(e);
                                                      };
     di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f);
+    m_pdd_grobner.get_stats().m_conflicts++;
 }
 
 void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {