diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 291af3b5c..970eb991f 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -62,6 +62,10 @@ namespace dd {
         init_nodes(level2var);
     }
 
+    void pdd_manager::set_max_num_nodes(unsigned n) {        
+        m_max_num_nodes = n + m_level2var.size();
+    }
+
     void pdd_manager::init_nodes(unsigned_vector const& l2v) {
         // add dummy nodes for operations, and 0, 1 pdds.
         for (unsigned i = 0; i < pdd_no_op; ++i) {
@@ -1352,9 +1356,8 @@ namespace dd {
             e->get_data().m_refcount = 0;      
         }
         if (do_gc) {
-            if (m_nodes.size() > m_max_num_nodes) {
-                throw mem_out();
-            }
+            if (m_nodes.size() > m_max_num_nodes) 
+                throw mem_out();            
             alloc_free_nodes(m_nodes.size()/2);
         }
         SASSERT(e->get_data().m_lo == n.m_lo);
@@ -1600,7 +1603,8 @@ namespace dd {
         for (unsigned i = m_nodes.size(); i-- > pdd_no_op; ) {
             if (!reachable[i]) {
                 if (is_val(i)) {
-                    if (m_freeze_value == val(i)) continue;
+                    if (m_freeze_value == val(i)) 
+                        continue;
                     m_free_values.push_back(m_mpq_table.find(val(i)).m_value_index);
                     m_mpq_table.remove(val(i));  
                 }
@@ -1615,20 +1619,17 @@ namespace dd {
 
         ptr_vector<op_entry> to_delete, to_keep;
         for (auto* e : m_op_cache) {            
-            if (e->m_result != null_pdd) {
-                to_delete.push_back(e);
-            }
-            else {
-                to_keep.push_back(e);
-            }
+            if (e->m_result != null_pdd)
+                to_delete.push_back(e);            
+            else 
+                to_keep.push_back(e);            
         }
         m_op_cache.reset();
-        for (op_entry* e : to_delete) {
+        for (op_entry* e : to_delete) 
             m_alloc.deallocate(sizeof(*e), e);
-        }
-        for (op_entry* e : to_keep) {
-            m_op_cache.insert(e);
-        }
+        
+        for (op_entry* e : to_keep) 
+            m_op_cache.insert(e);        
 
         m_factor_cache.reset();
 
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 6dee7977f..f2547e962 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -324,8 +324,9 @@ namespace dd {
         semantics get_semantics() const { return m_semantics; }
 
         void reset(unsigned_vector const& level2var);
-        void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
+        void set_max_num_nodes(unsigned n);
         unsigned_vector const& get_level2var() const { return m_level2var; }
+        unsigned num_nodes() const { return m_nodes.size() - m_free_nodes.size(); }
 
         pdd mk_var(unsigned i);
         pdd mk_val(rational const& r);
diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp
index 8673d87f3..6364d9ae6 100644
--- a/src/math/grobner/pdd_simplifier.cpp
+++ b/src/math/grobner/pdd_simplifier.cpp
@@ -75,7 +75,7 @@ namespace dd {
             }
         }
         catch (pdd_manager::mem_out) {
-            IF_VERBOSE(2, verbose_stream() << "simplifier memout\n");
+            IF_VERBOSE(1, verbose_stream() << "simplifier memout\n");
             // done reduce
             DEBUG_CODE(s.invariant(););
         }
@@ -94,7 +94,8 @@ namespace dd {
         for (equation* e : s.m_to_simplify) {
             pdd p = e->poly();
             if (binary) {
-                if (p.is_binary()) linear.push_back(e);
+                if (p.is_binary()) 
+                    linear.push_back(e);
             }
             else if (p.is_linear()) {
                 linear.push_back(e);
@@ -112,29 +113,33 @@ namespace dd {
         use_list_t use_list = get_use_list();
         compare_top_var ctv;
         std::stable_sort(linear.begin(), linear.end(), ctv);
-        equation_vector trivial;
+        struct trivial {
+            solver& s;
+            equation_vector elems;
+            trivial(solver& s) : s(s) {}
+            ~trivial () {
+                for (auto* e : elems)
+                    s.del_equation(e);
+            }
+        };
+        trivial trivial(s);
         unsigned j = 0;
         bool has_conflict = false;
         for (equation* src : linear) {
-            if (has_conflict) {
-                break;
-            }
-            if (s.is_trivial(*src)) {
-                continue;
-            }
+            if (has_conflict) 
+                break;            
+            if (s.is_trivial(*src)) 
+                continue;            
             unsigned v = src->poly().var();
             equation_vector const& uses = use_list[v];
             TRACE("dd.solver", 
                   s.display(tout << "uses of: ", *src) << "\n";
-                  for (equation* e : uses) {
-                      s.display(tout, *e) << "\n";
-                  });
+                  for (equation* e : uses) s.display(tout, *e) << "\n";);
             bool changed_leading_term;
             bool all_reduced = true;
             for (equation* dst : uses) {
-                if (src == dst || s.is_trivial(*dst)) {
-                    continue;                    
-                }
+                if (src == dst || s.is_trivial(*dst)) 
+                    continue;                                    
                 pdd q = dst->poly();
                 if (!src->poly().is_binary() && !q.is_linear()) {
                     all_reduced = false;
@@ -142,9 +147,8 @@ namespace dd {
                 }
                 remove_from_use(dst, use_list, v);
                 s.simplify_using(*dst, *src, changed_leading_term);
-                if (s.is_trivial(*dst)) {
-                    trivial.push_back(dst);
-                }
+                if (s.is_trivial(*dst)) 
+                    trivial.elems.push_back(dst);                
                 else if (s.is_conflict(dst)) {
                     s.pop_equation(dst);
                     s.set_conflict(dst);
@@ -158,9 +162,8 @@ namespace dd {
                 // SASSERT(!dst->poly().free_vars().contains(v));
                 add_to_use(dst, use_list);  
             }          
-            if (all_reduced) {
-                linear[j++] = src;              
-            }
+            if (all_reduced) 
+                linear[j++] = src;                          
         }
         if (!has_conflict) {
             linear.shrink(j);      
@@ -169,9 +172,7 @@ namespace dd {
                 s.push_equation(solver::solved, src);
             }
         }
-        for (equation* e : trivial) {
-            s.del_equation(e);
-        }
+                    
         DEBUG_CODE(s.invariant(););
         return j > 0 || has_conflict;
     }
@@ -187,8 +188,9 @@ namespace dd {
         IF_VERBOSE(3, verbose_stream() << "cc\n");
         u_map<equation*> los;
         bool reduced = false;
-        unsigned j = 0;
-        for (equation* eq1 : s.m_to_simplify) {
+        solver::scoped_update sc(s.m_to_simplify);
+        for (; sc.i < sc.sz; ++sc.i) {
+            auto* eq1 = sc.get();
             SASSERT(eq1->state() == solver::to_simplify);
             pdd p = eq1->poly();
             equation* eq2 = los.insert_if_not_there(p.lo().index(), eq1);
@@ -201,14 +203,11 @@ namespace dd {
                     s.retire(eq1);
                     continue;
                 }
-                else if (s.check_conflict(*eq1)) {
-                    continue;
-                }
+                else if (s.check_conflict(*eq1)) 
+                    continue;                
             }
-            s.m_to_simplify[j] = eq1;
-            eq1->set_index(j++);
+            sc.nextj();
         }
-        s.m_to_simplify.shrink(j);
         return reduced;
     }
 
@@ -225,15 +224,12 @@ namespace dd {
             pdd p = e->poly();
             if (p.is_val())
                 continue;
-            if (!p.hi().is_val()) {
-                continue;
-            }
+            if (!p.hi().is_val()) 
+                continue;            
             leaves.reset();
-            for (equation* e2 : use_list[p.var()]) {
-                if (e != e2 && e2->poly().var_is_leaf(p.var())) {
-                    leaves.push_back(e2);
-                }
-            }
+            for (equation* e2 : use_list[p.var()]) 
+                if (e != e2 && e2->poly().var_is_leaf(p.var())) 
+                    leaves.push_back(e2);                            
             for (equation* e2 : leaves) {
                 bool changed_leading_term;
                 remove_from_use(e2, use_list);
@@ -263,23 +259,20 @@ namespace dd {
     bool simplifier::simplify_elim_pure_step() {
         TRACE("dd.solver", tout << "pure\n";);
         IF_VERBOSE(3, verbose_stream() << "pure\n");
-        use_list_t use_list = get_use_list();        
-        unsigned j = 0;
-        for (equation* e : s.m_to_simplify) {
+        use_list_t use_list = get_use_list();   
+        solver::scoped_update sc(s.m_to_simplify);
+        bool has_solved = false;
+        for (; sc.i < sc.sz; ++sc.i) {
+            equation* e = sc.get();
             pdd p = e->poly();
             if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
                 s.push_equation(solver::solved, e);
+                has_solved = true;
             }
-            else {
-                s.m_to_simplify[j] = e;
-                e->set_index(j++);
-            }
+            else
+                sc.nextj();
         }
-        if (j != s.m_to_simplify.size()) {
-            s.m_to_simplify.shrink(j);
-            return true;
-        }
-        return false;
+        return has_solved;
     }
 
     /**
@@ -288,63 +281,59 @@ namespace dd {
      */
     bool simplifier::simplify_elim_dual_step() {
         use_list_t use_list = get_use_list();        
-        unsigned j = 0;
         bool reduced = false;
-        for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) {
-            equation* e = s.m_to_simplify[i];            
-            pdd p = e->poly();
-            // check that e is linear in top variable.
-            if (e->state() != solver::to_simplify) {
-                reduced = true;
-            }
-            else if (!s.done() && !s.is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
-                for (equation* e2 : use_list[p.var()]) {
-                    if (e2 == e) continue;
-                    bool changed_leading_term;
-
-                    remove_from_use(e2, use_list);
-                    s.simplify_using(*e2, *e, changed_leading_term);
-                    if (s.is_conflict(e2)) {
-                        s.pop_equation(e2);
-                        s.set_conflict(e2);
-                    }
-                    // when e2 is trivial, leading term is changed
-                    SASSERT(!s.is_trivial(*e2) || changed_leading_term);
-                    if (changed_leading_term) {
-                        s.pop_equation(e2);
-                        s.push_equation(solver::to_simplify, e2);
-                    }
-                    add_to_use(e2, use_list);
-                    break;
+        {
+            solver::scoped_update sc(s.m_to_simplify);
+            for (; sc.i < sc.sz; ++sc.i) {
+                equation* e = sc.get();
+                pdd p = e->poly();
+                // check that e is linear in top variable.
+                if (e->state() != solver::to_simplify) {
+                    reduced = true;
                 }
-                reduced = true;
-                s.push_equation(solver::solved, e);
-            }
-            else {
-                s.m_to_simplify[j] = e;
-                e->set_index(j++);
+                else if (!s.done() && !s.is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
+                    for (equation* e2 : use_list[p.var()]) {
+                        if (e2 == e)
+                            continue;
+                        bool changed_leading_term;
+
+                        remove_from_use(e2, use_list);
+                        s.simplify_using(*e2, *e, changed_leading_term);
+                        if (s.is_conflict(e2)) {
+                            s.pop_equation(e2);
+                            s.set_conflict(e2);
+                        }
+                        // when e2 is trivial, leading term is changed
+                        SASSERT(!s.is_trivial(*e2) || changed_leading_term);
+                        if (changed_leading_term) {
+                            s.pop_equation(e2);
+                            s.push_equation(solver::to_simplify, e2);
+                        }
+                        add_to_use(e2, use_list);
+                        break;
+                    }
+                    reduced = true;
+                    s.push_equation(solver::solved, e);
+                }
+                else
+                    sc.nextj();
             }
         }
         if (reduced) {
             // clean up elements in s.m_to_simplify 
             // they may have moved.
-            s.m_to_simplify.shrink(j);
-            j = 0;
-            for (equation* e : s.m_to_simplify) {
-                if (s.is_trivial(*e)) {
-                    s.retire(e);
-                }
-                else if (e->state() == solver::to_simplify) {
-                    s.m_to_simplify[j] = e;
-                    e->set_index(j++);
-                }
+            solver::scoped_update sc(s.m_to_simplify);
+            for (; sc.i < sc.sz; ++sc.i) {
+                equation* e = sc.get();
+                if (s.is_trivial(*e)) 
+                    s.retire(e);                
+                else if (e->state() == solver::to_simplify)
+                    sc.nextj();
             }
-            s.m_to_simplify.shrink(j);
             return true;
         }
-        else {
-            return false;
-        }
+        else 
+            return false;        
     }
 
     void simplifier::add_to_use(equation* e, use_list_t& use_list) {
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index e689c78a9..3f41d07cf 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -90,11 +90,9 @@ namespace dd {
         
     }
     void solver::saturate() {
-        simplify();
-        if (done()) {
-            return;
-        }
-        init_saturate();
+        if (done()) 
+            return;        
+        init_saturate();  
         TRACE("dd.solver", display(tout););
         try {
             while (!done() && step()) {
@@ -105,7 +103,7 @@ namespace dd {
             DEBUG_CODE(invariant(););
         }
         catch (pdd_manager::mem_out) {
-            IF_VERBOSE(2, verbose_stream() << "mem-out\n");
+            IF_VERBOSE(1, verbose_stream() << "mem-out saturate\n");
             // don't reduce further
         }
     }
@@ -124,7 +122,7 @@ namespace dd {
 
     solver::scoped_process::~scoped_process() {
         if (e) {
-            pdd p = e->poly();
+            pdd const& p = e->poly();
             SASSERT(!p.is_val());
             g.push_equation(processed, e);            
         }
@@ -137,9 +135,8 @@ namespace dd {
 
 
     void solver::superpose(equation const & eq) {
-        for (equation* target : m_processed) {
-            superpose(eq, *target);
-        }
+        for (equation* target : m_processed) 
+            superpose(eq, *target);        
     }
 
     /*
@@ -166,32 +163,28 @@ namespace dd {
         TRACE("dd.solver", display(tout << "simplification result: ", eq););
     }
 
+    void solver::well_formed() {
+        auto& set = m_to_simplify;
+        for (unsigned k = 0; k < set.size(); ++k)
+            for (unsigned l = k + 1; l < set.size(); ++l) {
+                if (!set[l] || !set[k] || set[k] != set[l])
+                    continue;
+                verbose_stream() << k << " " << l << " " << set[k] << "\n";
+                for (auto* s : set)
+                    verbose_stream() << s->idx() << "\n";
+                VERIFY(set[k] != set[l]);
+            }
+    }
     /*
       Use the given equation to simplify equations in set
     */
-    void solver::simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier) {   
-        struct scoped_update {
-            equation_vector& set;
-            unsigned i, j, sz;
-            scoped_update(equation_vector& set): set(set), i(0), j(0), sz(set.size()) {}
-            void nextj() {
-                set[j] = set[i];
-                set[i]->set_index(j++);
-            }
-            ~scoped_update() {                
-                for (; i < sz; ++i) 
-                    nextj();
-                set.shrink(j);
-            }
-        };
-
+    void solver::simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier) {           
         scoped_update sr(set);
         for (; sr.i < sr.sz; ++sr.i) {
             equation& target = *set[sr.i];
             bool changed_leading_term = false;
             bool simplified = true;
             simplified = !done() && simplifier(target, changed_leading_term);
-
             
             if (simplified && is_trivial(target)) 
                 retire(&target);
@@ -286,21 +279,32 @@ namespace dd {
         m_stats.m_compute_steps++;
         IF_VERBOSE(3, if (m_stats.m_compute_steps % 100 == 0) verbose_stream() << "compute steps = " << m_stats.m_compute_steps << "\n";);
         equation* e = pick_next();
-        if (!e) return false;
+        if (!e) 
+            return false;
         scoped_process sd(*this, e);
         equation& eq = *e;
         SASSERT(eq.state() == to_simplify);
         simplify_using(eq, m_processed);
-        if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
-        if (check_conflict(eq)) { sd.e = nullptr; return false; }
+        if (is_trivial(eq)) { 
+            sd.e = nullptr; 
+            retire(e); 
+            return true; 
+        }
+        if (check_conflict(eq)) { 
+            sd.e = nullptr; 
+            return false; 
+        }
         m_too_complex = false;
         simplify_using(m_processed, eq);
-        if (done()) return false;
+        if (done()) 
+            return false;
         TRACE("dd.solver", display(tout << "eq = ", eq););
         superpose(eq);
         simplify_using(m_to_simplify, eq);
-        if (done()) return false;
-        if (!m_too_complex) sd.done();
+        if (done()) 
+            return false;
+        if (!m_too_complex) 
+            sd.done();
         return true;
     }
 
@@ -345,9 +349,9 @@ namespace dd {
     }
 
     void solver::reset() {
-        for (equation* e : m_solved) dealloc(e);
-        for (equation* e : m_to_simplify) dealloc(e);
-        for (equation* e : m_processed) dealloc(e);
+        for (equation* e : m_solved) dealloc(e);        
+        for (equation* e : m_to_simplify) dealloc(e);        
+        for (equation* e : m_processed) dealloc(e);        
         m_subst.reset();
         m_solved.reset();
         m_processed.reset();
@@ -445,7 +449,6 @@ namespace dd {
 #endif
     }
 
-
     void solver::pop_equation(equation& eq) {
         equation_vector& v = get_queue(eq);
         unsigned idx = eq.idx();
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index bc20c21b4..9ad3faee2 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -108,6 +108,7 @@ public:
 private:
 
     typedef ptr_vector<equation> equation_vector;
+            for (; i < sz; ++i)
     typedef std::function<void (u_dependency* d, std::ostream& out)> print_dep_t;
 
     pdd_manager&                                 m;