diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 3934f549e..86e569b09 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -46,6 +46,7 @@ namespace dd {
     public:
         enum semantics { free_e, mod2_e, zero_one_vars_e };
     private:
+        friend test;
         friend pdd;
         friend pdd_iterator;
 
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 2c0f4de53..337ce6b7c 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -83,7 +83,7 @@ namespace dd {
         cfg.m_expr_size_limit *= cfg.m_expr_size_growth;
         cfg.m_expr_degree_limit *= cfg.m_expr_degree_growth;;
         
-        IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold to 10 * " << 10 * ceil(log(m_to_simplify.size())) << "* " << m_to_simplify.size() << " = " <<  m_config.m_eqs_threshold  << "\n";
+        IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold " <<  m_config.m_eqs_threshold  << "\n";
                    verbose_stream() << "set m_config.m_expr_size_limit to " <<  m_config.m_expr_size_limit << "\n";
                    verbose_stream() << "set m_config.m_expr_degree_limit to " <<  m_config.m_expr_degree_limit << "\n";
                    );
@@ -91,6 +91,9 @@ namespace dd {
     }
     void solver::saturate() {
         simplify();
+        if (done()) {
+            return;
+        }
         init_saturate();
         TRACE("dd.solver", display(tout););
         try {
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index c4456f2a6..89146b5b3 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1452,16 +1452,8 @@ void core::configure_grobner() {
     }
 #endif
    
-    double tree_size = 100;
-    unsigned gr_eq_size = 0;
-    for (auto* e : m_pdd_grobner.equations()) {
-        tree_size = std::max(tree_size, e->poly().tree_size());
-        gr_eq_size ++;
-    }
-    tree_size *= 10;
     struct dd::solver::config cfg;
-    cfg.m_expr_size_limit = (unsigned)tree_size;
-    cfg.m_max_steps = gr_eq_size;
+    cfg.m_max_steps = m_pdd_grobner.equations().size();
     cfg.m_max_simplified = m_nla_settings.grobner_max_simplified();
     cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth();
     cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth();
diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg
index 0e0c5df15..005b738be 100644
--- a/src/math/lp/nla_params.pyg
+++ b/src/math/lp/nla_params.pyg
@@ -9,8 +9,8 @@ def_module_params('nla',
                    ('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
                    ('grobner', BOOL, True, 'run grobner\'s basis heuristic'),
                    ('grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '),
-                   ('grobner_expr_size_growth', UINT, 10, 'grobner\'s maximum expr size growth'),
-                   ('grobner_expr_degree_growth', UINT, 10, 'grobner\'s maximum expr degree growth'),
+                   ('grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'),
+                   ('grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
                    ('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
                    ('grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                    ('grobner_subs_fixed', BOOL, False, 'substitute fixed variables by constants')