diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 29174e31f..ed1ba733a 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -127,7 +127,7 @@ namespace dd {
 
     void solver::saturate() {
         simplify();
-        tuned_init();
+        init_saturate();
         TRACE("dd.solver", display(tout););
         try {
             while (!done() && step()) {
@@ -144,11 +144,6 @@ namespace dd {
         }
     }
 
-    bool solver::step() {
-        m_stats.m_compute_steps++;
-        return tuned_step();
-    }
-
     void solver::scoped_process::done() {
         pdd p = e->poly();
         SASSERT(!p.is_val());
@@ -167,19 +162,7 @@ namespace dd {
             SASSERT(!p.is_val());
             g.push_equation(processed, e);            
         }
-    }
-
-    
-    solver::equation* solver::pick_next() {
-        equation* eq = nullptr;
-        for (auto* curr : m_to_simplify) {
-            if (!eq || is_simpler(*curr, *eq)) {
-                eq = curr;
-            }
-        }
-        if (eq) pop_equation(eq);
-        return eq;
-    }
+    }    
 
     void solver::simplify() {
         try {
@@ -639,8 +622,9 @@ namespace dd {
         }
     }
 
-    bool solver::tuned_step() {
-        equation* e = tuned_pick_next();
+    bool solver::step() {
+        m_stats.m_compute_steps++;
+        equation* e = pick_next();
         if (!e) return false;
         scoped_process sd(*this, e);
         equation& eq = *e;
@@ -660,7 +644,7 @@ namespace dd {
         return true;
     }
 
-    void solver::tuned_init() {
+    void solver::init_saturate() {
         unsigned_vector const& l2v = m.get_level2var();
         m_level2var.resize(l2v.size());
         m_var2level.resize(l2v.size());
@@ -714,7 +698,7 @@ namespace dd {
         watch.shrink(j);        
     }
 
-    solver::equation* solver::tuned_pick_next() {
+    solver::equation* solver::pick_next() {
         while (m_levelp1 > 0) {
             unsigned v = m_level2var[m_levelp1-1];
             equation_vector const& watch = m_watch[v];
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index c09e6723e..e3a2fe398 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -142,15 +142,12 @@ private:
     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;  }
 
-    // tuned implementation
     vector<equation_vector> m_watch;           // watch list mapping variables to vector of equations where they occur (generally a subset)
     unsigned                m_levelp1;         // index into level+1
     unsigned_vector         m_level2var;       // level -> var
     unsigned_vector         m_var2level;       // var -> level
 
-    bool tuned_step();
-    void tuned_init();
-    equation* tuned_pick_next();
+    void init_saturate();
     void simplify_watch(equation const& eq);
     void add_to_watch(equation& eq);
 
diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp
index d10532735..cf4e3ca7a 100644
--- a/src/test/pdd_solver.cpp
+++ b/src/test/pdd_solver.cpp
@@ -11,9 +11,9 @@
 #include "tactic/bv/bit_blaster_tactic.h"
 
 namespace dd {
-    void print_eqs(ptr_vector<grobner::equation> const& eqs) {
+    void print_eqs(ptr_vector<solver::equation> const& eqs) {
         std::cout << "eqs\n";
-        for (grobner::equation* e : eqs) {
+        for (solver::equation* e : eqs) {
             std::cout << e->poly() << "\n";
         }
     }
@@ -25,7 +25,7 @@ namespace dd {
         pdd v2 = m.mk_var(2);
         pdd v3 = m.mk_var(3);
         
-        grobner gb(lim, m);
+        solver gb(lim, m);
         gb.add(v1*v2 + v1*v3);
         gb.add(v1 - 1);
         gb.display(std::cout);
@@ -142,7 +142,7 @@ namespace dd {
         return expr_ref(cache[e], m);
     }
 
-    void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) {
+    void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, solver& g) {
         expr* a, *b;
         pdd v1 = p.mk_var(id2var[e->get_id()]);
         pdd q(p);
@@ -200,7 +200,7 @@ namespace dd {
 
         collect_id2var(id2var, fmls);
         pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e);
-        grobner g(m.limit(), p);
+        solver g(m.limit(), p);
 
         for (expr* e : subterms(fmls)) {
             add_def(id2var, to_app(e), m, p, g);