diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index d1ef03533..aee5e8535 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -126,6 +126,8 @@ namespace dd {
             if (simplify_source_target(eq, *target, changed_leading_term)) {
                 if (is_trivial(*target))
                     to_delete.push_back(target);
+                else if (is_too_complex(*target))
+                    to_delete.push_back(target);
                 else if (check_conflict(*target))
                     return false;
                 else if (changed_leading_term && target->is_processed()) {
@@ -170,6 +172,7 @@ namespace dd {
         if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return;
         m_stats.m_superposed++;
         if (r.is_zero()) return;
+        if (is_too_complex(r)) return;
         equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size());
         m_equations.push_back(eq);
         update_stats_max_degree_and_size(*eq);
diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h
index bdf123369..f89f54e83 100644
--- a/src/math/grobner/pdd_grobner.h
+++ b/src/math/grobner/pdd_grobner.h
@@ -119,6 +119,9 @@ private:
     bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
     bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(), true); }    
     void set_conflict() { m_conflict = true; }
+    bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
+    bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit;  }
+
 
     void del_equations(unsigned old_size);
     void del_equation(equation* eq);