diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 13451f270..012791eb5 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -723,6 +723,7 @@ namespace dd {
         bool do_gc = m_free_nodes.empty();
         if (do_gc && !m_disable_gc) {
             gc();
+            SASSERT(n.m_hi == 0 || (!m_free_nodes.contains(n.m_hi) && !m_free_nodes.contains(n.m_lo)));            
             e = m_node_table.insert_if_not_there2(n);
             e->get_data().m_refcount = 0;      
         }
diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 3aab98e4f..329c08f92 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -56,8 +56,8 @@ void grobner::del_equations(unsigned old_size) {
 }
 
 void grobner::del_equation(equation * eq) {
-    m_to_superpose.erase(eq);
-    m_to_simplify.erase(eq);
+    m_processed.erase(eq);
+    m_to_process.erase(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
     m_equations_to_delete[eq->m_bidx] = 0;
     del_monomials(eq->m_monomials);
@@ -85,11 +85,36 @@ void grobner::unfreeze_equations(unsigned old_size) {
     it += old_size;
     for (; it != end; ++it) {
         equation * eq = *it;
-        m_to_simplify.insert(eq);
+        m_to_process.insert(eq);
     }
     m_equations_to_unfreeze.shrink(old_size);
 }
 
+void grobner::push_scope() {
+    m_scopes.push_back(scope());
+    scope & s = m_scopes.back();
+    s.m_equations_to_unfreeze_lim = m_equations_to_unfreeze.size();
+    s.m_equations_to_delete_lim   = m_equations_to_delete.size();
+}
+
+void grobner::pop_scope(unsigned num_scopes) {
+    SASSERT(num_scopes >= get_scope_level());
+    unsigned new_lvl = get_scope_level() - num_scopes;
+    scope & s        = m_scopes[new_lvl];
+    unfreeze_equations(s.m_equations_to_unfreeze_lim);
+    del_equations(s.m_equations_to_delete_lim);
+    m_scopes.shrink(new_lvl);
+}
+
+void grobner::reset() {
+    flush();
+    m_processed.reset();
+    m_to_process.reset();
+    m_equations_to_unfreeze.reset();
+    m_equations_to_delete.reset();
+    m_unsat = nullptr;
+}
+
 void grobner::display_var(std::ostream & out, expr * var) const {
     if (is_app(var) && to_app(var)->get_num_args() > 0)
         out << mk_bounded_pp(var, m_manager);
@@ -163,8 +188,8 @@ void grobner::display_equations(std::ostream & out, equation_set const & v, char
 }
 
 void grobner::display(std::ostream & out) const {
-    display_equations(out, m_to_superpose, "m_to_superpose:");
-    display_equations(out, m_to_simplify, "m_to_simplify:");
+    display_equations(out, m_processed, "processed:");
+    display_equations(out, m_to_process, "to process:");
 }
 
 void grobner::set_weight(expr * n, int weight) {
@@ -196,7 +221,7 @@ void grobner::update_order(equation_set & s, bool processed) {
         if (update_order(eq)) {
             if (processed) {
                 to_remove.push_back(eq);
-                m_to_simplify.insert(eq);
+                m_to_process.insert(eq);
             }
         }
     }
@@ -205,8 +230,8 @@ void grobner::update_order(equation_set & s, bool processed) {
 }
 
 void grobner::update_order() {
-    update_order(m_to_simplify, false);
-    update_order(m_to_superpose, true);
+    update_order(m_to_process, false);
+    update_order(m_processed, true);
 }
 
 bool grobner::var_lt::operator()(expr * v1, expr * v2) const {
@@ -287,6 +312,7 @@ grobner::monomial * grobner::mk_monomial(rational const & coeff, expr * m) {
 }
 
 void grobner::init_equation(equation * eq, v_dependency * d) {
+    eq->m_scope_lvl = get_scope_level();
     unsigned bidx   = m_equations_to_delete.size();
     eq->m_bidx      = bidx;
     eq->m_dep       = d;
@@ -305,7 +331,7 @@ void grobner::assert_eq_0(unsigned num_monomials, monomial * const * monomials,
         equation * eq       = alloc(equation); 
         eq->m_monomials.swap(ms);
         init_equation(eq, ex);                                                   
-        m_to_simplify.insert(eq);
+        m_to_process.insert(eq);
     }
 }
 
@@ -321,7 +347,7 @@ void grobner::assert_eq_0(unsigned num_monomials, rational const * coeffs, expr
         normalize_coeff(ms);                            \
         eq->m_monomials.swap(ms);                       \
         init_equation(eq, ex);                          \
-        m_to_simplify.insert(eq);                        \
+        m_to_process.insert(eq);                        \
     }
 
     MK_EQ(coeffs[i]);
@@ -371,7 +397,7 @@ void grobner::assert_monomial_tautology(expr * m) {
     eq->m_monomials.push_back(m1);
     normalize_coeff(eq->m_monomials);                                          
     init_equation(eq, static_cast<v_dependency*>(nullptr));                                                          \
-    m_to_simplify.insert(eq);
+    m_to_process.insert(eq);
 }
 
 /**
@@ -450,7 +476,7 @@ void grobner::normalize_coeff(ptr_vector<monomial> & monomials) {
 /**
    \brief Simplify the given monomials
 */
-void grobner::simplify_ptr_monomials(ptr_vector<monomial> & monomials) {
+void grobner::simplify(ptr_vector<monomial> & monomials) {
     std::stable_sort(monomials.begin(), monomials.end(), m_monomial_lt);
     merge_monomials(monomials);
     normalize_coeff(monomials);
@@ -476,22 +502,19 @@ inline bool grobner::is_trivial(equation * eq) const {
 /**
    \brief Sort monomials, and merge monomials with the same body.
 */
-void grobner::simplify_eq(equation * eq) {
-    simplify_ptr_monomials(eq->m_monomials);
+void grobner::simplify(equation * eq) {
+    simplify(eq->m_monomials);
     if (is_inconsistent(eq) && !m_unsat)
         m_unsat = eq;
 }
 
 /**
    \brief Return true if monomial m1 is (* c1 M) and m2 is (* c2 M M').
-   Store M' in m_tmp_vars1.
+   Store M' in rest.
    
    \remark This method assumes the variables of m1 and m2 are sorted.
 */
-bool grobner::divide_ignore_coeffs(monomial const * m2, monomial const * m1) {
-    SASSERT(m1 != m2);
-    ptr_vector<expr>  & rest = m_tmp_vars1;
-    rest.reset();
+bool grobner::is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const {
     unsigned i1  = 0;
     unsigned i2  = 0;
     unsigned sz1 = m1->m_vars.size();
@@ -532,11 +555,12 @@ bool grobner::divide_ignore_coeffs(monomial const * m2, monomial const * m1) {
 }
 
 /**
-   \brief Multiply the monomials of source starting at position start_idx by (coeff * vars), and store the resultant monomials in m_tmp_monomials
+   \brief Multiply the monomials of source starting at position start_idx by (coeff * vars), and store the resultant monomials
+   at result.
 */
-void grobner::mul_append_skip_first(equation const * source, rational const & coeff, ptr_vector<expr> const & vars) {
+void grobner::mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result) {
     unsigned sz = source->get_num_monomials();
-    for (unsigned i = 1; i < sz; i++) {
+    for (unsigned i = start_idx; i < sz; i++) {
         monomial const * m = source->get_monomial(i);
         monomial * new_m   = alloc(monomial);
         new_m->m_coeff     = m->m_coeff;
@@ -546,7 +570,7 @@ void grobner::mul_append_skip_first(equation const * source, rational const & co
         for (expr* e : new_m->m_vars) 
             m_manager.inc_ref(e);
         std::stable_sort(new_m->m_vars.begin(), new_m->m_vars.end(), m_var_lt);
-        m_tmp_monomials.push_back(new_m);
+        result.push_back(new_m);
     }
 }
 
@@ -574,65 +598,67 @@ grobner::equation * grobner::copy_equation(equation const * eq) {
     return r;
 }
 
-// source 3f + k = 0, so f = -k/3
-// target 2fg + e = 0  
-// target is replaced by 2(-k/3)g + e = -2/3kg + e
-bool grobner::simplify_target_monomials(equation const * source, equation * target) {
-    unsigned i          = 0;
-    unsigned new_target_sz = 0;
-    unsigned target_sz         = target->m_monomials.size();
-    monomial const * LT = source->get_monomial(0);
-    m_tmp_monomials.reset();
-    for (; i < target_sz; i++) {
-        monomial * targ_i = target->m_monomials[i];
-        if (divide_ignore_coeffs(targ_i, LT)) {
-            if (i == 0)
-                m_changed_leading_term = true;
-            if (!m_tmp_vars1.empty())
-                target->m_lc = false;
-            mul_append_skip_first(source, - targ_i->m_coeff / (LT->m_coeff), m_tmp_vars1);
-            del_monomial(targ_i);
-        }
-        else {
-            if (i != new_target_sz) {
-                target->m_monomials[new_target_sz] = targ_i;
-            }
-            new_target_sz++;
-        }
-    }
-    if (new_target_sz < target_sz) {
-        target->m_monomials.shrink(new_target_sz);
-        target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
-        simplify_eq(target);
-        TRACE("grobner", tout << "result: "; display_equation(tout, *target););
-        return true;
-    }
-    return false;
-}
-
 /**
    \brief Simplify the target equation using the source as a rewrite rule.
    Return 0 if target was not simplified.
+   Return target if target was simplified but source->m_scope_lvl <= target->m_scope_lvl.
+   Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result.
 */
-grobner::equation * grobner::simplify_source_target(equation const * source, equation * target) {
+grobner::equation * grobner::simplify(equation const * source, equation * target) {
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
     if (source->get_num_monomials() == 0)
         return nullptr;
     m_stats.m_simplify++;
     bool result = false;
+    bool simplified;
     do {
-        if (simplify_target_monomials(source, target)) {
-            result = true;
-        } else {
-            break;
+        simplified          = false;
+        unsigned i          = 0;
+        unsigned j          = 0;
+        unsigned sz         = target->m_monomials.size();
+        monomial const * LT = source->get_monomial(0); 
+        ptr_vector<monomial> & new_monomials = m_tmp_monomials;
+        new_monomials.reset();
+        ptr_vector<expr>  & rest = m_tmp_vars1;
+        for (; i < sz; i++) {
+            monomial * curr = target->m_monomials[i];
+            rest.reset();
+            if (is_subset(LT, curr, rest)) {
+                if (i == 0)
+                    m_changed_leading_term = true;
+                if (source->m_scope_lvl > target->m_scope_lvl) {
+                    target = copy_equation(target);
+                    SASSERT(target->m_scope_lvl >= source->m_scope_lvl);
+                }
+                if (!result) {
+                    // first time that source is being applied.
+                    target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
+                }
+                simplified     = true;
+                result         = true;
+                rational coeff = curr->m_coeff;
+                coeff         /= LT->m_coeff;
+                coeff.neg();
+                if (!rest.empty())
+                    target->m_lc = false;
+                mul_append(1, source, coeff, rest, new_monomials);
+                del_monomial(curr);
+                target->m_monomials[i] = 0;
+            }
+            else {
+                target->m_monomials[j] = curr;
+                j++;
+            }
+        }
+        if (simplified) {
+            target->m_monomials.shrink(j);
+            target->m_monomials.append(new_monomials.size(), new_monomials.c_ptr());
+            simplify(target);
         }
-    } while (!m_manager.canceled());
-    TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
-    if (result) {
-        target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
-        return target;
     }
-    return nullptr;
+    while (simplified && !m_manager.canceled());
+    TRACE("grobner", tout << "result: "; display_equation(tout, *target););
+    return result ? target : nullptr;
 }
 
 /**
@@ -644,11 +670,11 @@ grobner::equation * grobner::simplify_source_target(equation const * source, equ
 grobner::equation * grobner::simplify_using_processed(equation * eq) {
     bool result = false;
     bool simplified;
-    TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities of size " << m_to_superpose.size() <<  "\n";);
+    TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities\n";);
     do {
         simplified = false;
-        for (equation const* p : m_to_superpose) {
-            equation * new_eq  = simplify_source_target(p, eq);
+        for (equation const* p : m_processed) {
+            equation * new_eq  = simplify(p, eq);
             if (new_eq) {
                 result     = true;
                 simplified = true;
@@ -687,7 +713,7 @@ bool grobner::is_better_choice(equation * eq1, equation * eq2) {
 grobner::equation * grobner::pick_next() {
     equation * r = nullptr;
     ptr_buffer<equation> to_delete;
-    for (equation * curr : m_to_simplify) {
+    for (equation * curr : m_to_process) {
         if (is_trivial(curr))
             to_delete.push_back(curr);
         else if (is_better_choice(curr, r))
@@ -696,82 +722,79 @@ grobner::equation * grobner::pick_next() {
     for (equation * e : to_delete) 
         del_equation(e);
     if (r)
-        m_to_simplify.erase(r);
+        m_to_process.erase(r);
     TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else display_equation(tout, *r););
     return r;
 }
 
-void grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
-    if (new_target != target) {
-        m_equations_to_unfreeze.push_back(target);
-        to_remove.push_back(target);
-        if (m_changed_leading_term) {
-            m_to_simplify.insert(new_target);
-            to_remove.push_back(target);
-        }
-        else {
-            to_insert.push_back(new_target);
-        }
-        target = new_target;
-    }
-    else {
-        if (m_changed_leading_term) {
-            m_to_simplify.insert(target);
-            to_remove.push_back(target);
-        }
-    }
-}
 /**
    \brief Use the given equation to simplify processed terms.
 */
-bool grobner::simplify_processed_with_eq(equation * eq) {
+bool grobner::simplify_processed(equation * eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
-    equation_set::iterator it  = m_to_superpose.begin();
-    equation_set::iterator end = m_to_superpose.end();
+    equation_set::iterator it  = m_processed.begin();
+    equation_set::iterator end = m_processed.end();
     for (; it != end && !m_manager.canceled(); ++it) {
-        equation * target        = *it;
+        equation * curr        = *it;
         m_changed_leading_term = false;
-        // if the leading term is simplified, then the equation has to be moved to m_to_simplify
-        equation * new_target    = simplify_source_target(eq, target);
-        if (new_target != nullptr) {
-            process_simplified_target(to_insert, new_target, target, to_remove);
+        // if the leading term is simplified, then the equation has to be moved to m_to_process
+        equation * new_curr    = simplify(eq, curr);
+        if (new_curr != nullptr) {
+            if (new_curr != curr) {
+                m_equations_to_unfreeze.push_back(curr);
+                to_remove.push_back(curr);
+                if (m_changed_leading_term) {
+                    m_to_process.insert(new_curr);
+                    to_remove.push_back(curr);
+                }
+                else {
+                    to_insert.push_back(new_curr);
+                }
+                curr = new_curr;
+            }
+            else {
+                if (m_changed_leading_term) {
+                    m_to_process.insert(curr);
+                    to_remove.push_back(curr);
+                }
+            }
         }
-        if (is_trivial(target))
-            to_delete.push_back(target);
+        if (is_trivial(curr))
+            to_delete.push_back(curr);
     }
     for (equation* eq : to_insert) 
-        m_to_superpose.insert(eq);
+        m_processed.insert(eq);
     for (equation* eq : to_remove)
-        m_to_superpose.erase(eq);
+        m_processed.erase(eq);
     for (equation* eq : to_delete) 
         del_equation(eq);
     return !m_manager.canceled();
 }
 
 /**
-   \brief Use the given equation to simplify m_to_simplify equation.
+   \brief Use the given equation to simplify to-process terms.
 */
-void grobner::simplify_m_to_simplify(equation * eq) {
+void grobner::simplify_to_process(equation * eq) {
     ptr_buffer<equation> to_insert;
     ptr_buffer<equation> to_remove;
     ptr_buffer<equation> to_delete;
-    for (equation* target : m_to_simplify) {
-        equation * new_target = simplify_source_target(eq, target);
-        if (new_target != nullptr && new_target != target) {
-            m_equations_to_unfreeze.push_back(target);
-            to_insert.push_back(new_target);
-            to_remove.push_back(target);
-            target = new_target;
+    for (equation* curr : m_to_process) {
+        equation * new_curr = simplify(eq, curr);
+        if (new_curr != nullptr && new_curr != curr) {
+            m_equations_to_unfreeze.push_back(curr);
+            to_insert.push_back(new_curr);
+            to_remove.push_back(curr);
+            curr = new_curr;
         }
-        if (is_trivial(target))
-            to_delete.push_back(target);
+        if (is_trivial(curr))
+            to_delete.push_back(curr);
     }
     for (equation* eq : to_insert)
-        m_to_simplify.insert(eq);
+        m_to_process.insert(eq);
     for (equation* eq : to_remove)
-        m_to_simplify.erase(eq);
+        m_to_process.erase(eq);
     for (equation* eq : to_delete)
         del_equation(eq);
 }
@@ -780,7 +803,7 @@ void grobner::simplify_m_to_simplify(equation * eq) {
    \brief If m1 = (* c M M1) and m2 = (* d M M2) and M is non empty, then return true and store M1 in rest1 and M2 in rest2.
 */
 bool grobner::unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2) {
-    TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " and "; display_monomial(tout, *m2); tout << "\n";);
+    TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " "; display_monomial(tout, *m2); tout << "\n";);
     bool found_M = false;
     unsigned i1  = 0;
     unsigned i2  = 0;
@@ -832,39 +855,35 @@ void grobner::superpose(equation * eq1, equation * eq2) {
     rest1.reset();
     ptr_vector<expr> & rest2 = m_tmp_vars2;
     rest2.reset();
-    TRACE("grobner", tout << "trying to superpose:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2);); 
     if (unify(eq1->m_monomials[0], eq2->m_monomials[0], rest1, rest2)) {
         TRACE("grobner", tout << "superposing:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2); 
               tout << "rest1: "; display_vars(tout, rest1.size(), rest1.c_ptr()); tout << "\n";
               tout << "rest2: "; display_vars(tout, rest2.size(), rest2.c_ptr()); tout << "\n";);
         ptr_vector<monomial> & new_monomials = m_tmp_monomials;
         new_monomials.reset();
-        mul_append_skip_first(eq1, eq2->m_monomials[0]->m_coeff, rest2);
+        mul_append(1, eq1, eq2->m_monomials[0]->m_coeff, rest2, new_monomials);
         rational c = eq1->m_monomials[0]->m_coeff;
         c.neg();
-        mul_append_skip_first(eq2, c, rest1);
-        simplify_ptr_monomials(new_monomials);
+        mul_append(1, eq2, c, rest1, new_monomials);
+        simplify(new_monomials);
         TRACE("grobner", tout << "resulting monomials: "; display_monomials(tout, new_monomials.size(), new_monomials.c_ptr()); tout << "\n";);
         if (new_monomials.empty())
             return;
         m_num_new_equations++;
-        TRACE("grobner", tout << "success superposing\n";);
         equation * new_eq = alloc(equation);
         new_eq->m_monomials.swap(new_monomials);
         init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep));
         new_eq->m_lc = false;
-        m_to_simplify.insert(new_eq);
-    } else {
-        TRACE("grobner", tout << "unify did not work\n";);
+        m_to_process.insert(new_eq);
     }
 }
 
 /**
-   \brief Superpose the given equations with the equations in m_to_superpose.
+   \brief Superpose the given equations with the equations in m_processed.
 */
 void grobner::superpose(equation * eq) {
-    for (equation * target : m_to_superpose) {
-        superpose(eq, target);
+    for (equation * curr : m_processed) {
+        superpose(eq, curr);
     }
 }
 
@@ -874,33 +893,26 @@ void grobner::compute_basis_init() {
 }
 
 bool grobner::compute_basis_step() {
-    TRACE("grobner", display(tout););
     equation * eq = pick_next();
-    if (!eq) 
+    if (!eq)
         return true;
     m_stats.m_num_processed++;
 #ifdef PROFILE_GB
-    if (m_stats.m_num_to_superpose % 100 == 0) {
-        verbose_stream() << "[grobner] " << m_to_superpose.size() << " " << m_to_simplify.size() << "\n";
+    if (m_stats.m_num_processed % 100 == 0) {
+        verbose_stream() << "[grobner] " << m_processed.size() << " " << m_to_process.size() << "\n";
     }
 #endif
     equation * new_eq = simplify_using_processed(eq);
-    if (new_eq == nullptr || new_eq->get_num_monomials() == 0) {
-        TRACE("grobner",);
-    }
     if (new_eq != nullptr && eq != new_eq) {
         // equation was updated using non destructive updates
         m_equations_to_unfreeze.push_back(eq);
         eq = new_eq;
     }
     if (m_manager.canceled()) return false;
-    if (!simplify_processed_with_eq(eq)) {
-        TRACE("grobner", tout << "end of iteration:\n"; display(tout););
-        return false;
-    }
+    if (!simplify_processed(eq)) return false;
     superpose(eq);
-    m_to_superpose.insert(eq);
-    simplify_m_to_simplify(eq);
+    m_processed.insert(eq);
+    simplify_to_process(eq);
     TRACE("grobner", tout << "end of iteration:\n"; display(tout););
     return false;
 }
@@ -908,10 +920,7 @@ bool grobner::compute_basis_step() {
 bool grobner::compute_basis(unsigned threshold) {
     compute_basis_init();
     while (m_num_new_equations < threshold && !m_manager.canceled()) {
-        if (compute_basis_step()) {
-            
-            return true;
-        }
+        if (compute_basis_step()) return true;
     }
     return false;
 }
@@ -922,12 +931,12 @@ void grobner::copy_to(equation_set const & s, ptr_vector<equation> & result) con
 }
 
 /**
-   \brief Copy the equations in m_to_superpose and m_to_simplify to result.
+   \brief Copy the equations in m_processed and m_to_process to result.
    
    \warning This equations can be deleted when compute_basis is invoked.
 */
 void grobner::get_equations(ptr_vector<equation> & result) const {
-    copy_to(m_to_superpose, result);
-    copy_to(m_to_simplify, result);
+    copy_to(m_processed, result);
+    copy_to(m_to_process, result);
 }
 
diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h
index ce44d08a4..9233866d5 100644
--- a/src/math/grobner/grobner.h
+++ b/src/math/grobner/grobner.h
@@ -58,6 +58,7 @@ public:
     };
 
     class equation {
+        unsigned             m_scope_lvl;     //!< scope level when this equation was created.
         unsigned             m_bidx:31;       //!< position at m_equations_to_delete
         unsigned             m_lc:1;          //!< true if equation if a linear combination of the input equations.
         ptr_vector<monomial> m_monomials;     //!< sorted monomials
@@ -97,8 +98,8 @@ protected:
     obj_map<expr, int>      m_var2weight;
     var_lt                  m_var_lt;
     monomial_lt             m_monomial_lt;
-    equation_set            m_to_superpose;
-    equation_set            m_to_simplify;
+    equation_set            m_processed;
+    equation_set            m_to_process;
     equation_vector         m_equations_to_unfreeze;
     equation_vector         m_equations_to_delete;
     bool                    m_changed_leading_term; // set to true, if the leading term was simplified.
@@ -107,6 +108,7 @@ protected:
         unsigned m_equations_to_unfreeze_lim;
         unsigned m_equations_to_delete_lim;
     };
+    svector<scope>          m_scopes;
     ptr_vector<monomial>    m_tmp_monomials;
     ptr_vector<monomial>    m_del_monomials;
     ptr_vector<expr>        m_tmp_vars1;
@@ -153,20 +155,19 @@ protected:
     
     void normalize_coeff(ptr_vector<monomial> & monomials);
 
-    void simplify_ptr_monomials(ptr_vector<monomial> & monomials);
+    void simplify(ptr_vector<monomial> & monomials);
 
-    void simplify_eq(equation * eq);
+    void simplify(equation * eq);
 
-    bool divide_ignore_coeffs(monomial const * m1, monomial const * m2);
+    bool is_subset(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest) const;
 
-    void mul_append_skip_first(equation const * source, rational const & coeff, ptr_vector<expr> const & vars);
+    void mul_append(unsigned start_idx, equation const * source, rational const & coeff, ptr_vector<expr> const & vars, ptr_vector<monomial> & result);
 
     monomial * copy_monomial(monomial const * m);
 
     equation * copy_equation(equation const * eq);
 
-    equation * simplify_source_target(equation const * source, equation * target);
-    bool simplify_target_monomials(equation const * source, equation * target);
+    equation * simplify(equation const * source, equation * target);
 
     equation * simplify_using_processed(equation * eq);
 
@@ -174,9 +175,9 @@ protected:
 
     equation * pick_next();
 
-    bool simplify_processed_with_eq(equation * eq);
+    bool simplify_processed(equation * eq);
 
-    void simplify_m_to_simplify(equation * eq);
+    void simplify_to_process(equation * eq);
 
     bool unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2);
 
@@ -191,6 +192,8 @@ public:
 
     ~grobner();
 
+    unsigned get_scope_level() const { return m_scopes.size(); }
+
     /**
        \brief Set the weight of a term that is viewed as a variable by this module.
        The weight is used to order monomials. If the weight is not set for a term t, then the
@@ -271,14 +274,19 @@ public:
     /**
        \brief Reset state. Remove all equalities asserted with assert_eq.
     */
+    void reset();
+
     void get_equations(ptr_vector<equation> & result) const;
     
+    void push_scope();
+
+    void pop_scope(unsigned num_scopes);
+
     void display_equation(std::ostream & out, equation const & eq) const;
 
     void display_monomial(std::ostream & out, monomial const & m) const;
 
     void display(std::ostream & out) const;
-    void process_simplified_target(ptr_buffer<equation>& to_delete, equation* new_curr, equation*& curr, ptr_buffer<equation>& to_remove);
 };
 
 #endif /* GROBNER_H_ */
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
new file mode 100644
index 000000000..c661ee4ef
--- /dev/null
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -0,0 +1,882 @@
+/*++
+  Copyright (c) 2019 Microsoft Corporation
+
+  Abstract:
+
+    Grobner core based on pdd representation of polynomials
+
+  Author:
+     Nikolaj Bjorner (nbjorner)
+     Lev Nachmanson (levnach)
+
+  --*/
+
+#include "math/grobner/pdd_grobner.h"
+#include "util/uint_set.h"
+
+namespace dd {
+
+    /***
+        A simple algorithm maintains two sets (S, A), 
+        where S is m_processed, and A is m_to_simplify.
+        Initially S is empty and A contains the initial equations.
+        
+        Each step proceeds as follows:
+        - pick a in A, and remove a from A
+        - simplify a using S
+        - simplify S using a
+        - for s in S:
+             b = superpose(a, s)
+             add b to A
+        - add a to S
+        - simplify A using a
+
+        Alternate:
+
+        - Fix a variable ordering x1 > x2 > x3 > ....
+        In each step:
+          - pick a in A with *highest* variable x_i in leading term of *lowest* degree.
+          - simplify a using S
+          - simplify S using a
+          - if a does not contains x_i, put it back into A and pick again (determine whether possible)
+          - for s in S:
+               b = superpose(a, s)
+               add b to A
+          - add a to S
+          - simplify A using a
+
+
+        Apply a watch list to filter out relevant elements of S
+        Index leading_term_watch: Var -> Equation*
+        Only need to simplify equations that contain eliminated variable.
+        The watch list can be used to index into equations that are useful to simplify.
+        A Bloom filter on leading term could further speed up test whether reduction applies.
+
+        For p in A:
+            populate watch list by maxvar(p) |-> p
+        For p in S:
+            do not occur in watch list
+
+        - the variable ordering should be chosen from a candidate model M, 
+          in a way that is compatible with weights that draw on the number of occurrences
+          in polynomials with violated evaluations and with the maximal slack (degree of freedom).
+         
+          weight(x) := < count { p in P | x in p, M(p) != 0 }, min_{p in P | x in p} slack(p,x) >
+
+          slack is computed from interval assignments to variables, and is an interval in which x can possibly move
+          (an over-approximation).
+
+        The alternative version maintains the following invariant:
+        - polynomials not in the watch list cannot be simplified using a
+          Justification:
+          - elements in S have no variables watched
+          - elements in A are always reduced modulo all variables above the current x_i.
+
+
+        TBD: 
+
+        Linear Elimination:
+        - comprises of a simplification pass that puts linear equations in to_processed
+        - so before simplifying with respect to the variable ordering, eliminate linear equalities.
+
+        Extended Linear Simplification (as exploited in Bosphorus AAAI 2019):
+        - multiply each polynomial by one variable from their orbits.
+        - The orbit of a varible are the variables that occur in the same monomial as it in some polynomial.
+        - The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts
+          additional linear equalities.
+        - Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices.
+
+        Long distance vanishing polynomials (used by PolyCleaner ICCAD 2019):
+        - identify polynomials p, q, such that p*q = 0
+        - main case is half-adders and full adders (p := x + y, q := x * y) over GF2
+          because (x+y)*x*y = 0 over GF2
+          To work beyond GF2 we would need to rely on simplification with respect to asserted equalities.
+          The method seems rather specific to hardware multipliers so not clear it is useful to 
+          generalize.
+        - find monomials that contain pairs of vanishing polynomials, transitively 
+          withtout actually inlining.
+          Then color polynomial variables w by p, resp, q if they occur in polynomial equalities
+          w - r = 0, such that all paths in r contain a node colored by p, resp q. 
+          polynomial variables that get colored by both p and q can be set to 0.
+          When some variable gets colored, other variables can be colored.
+        - We can walk pdd nodes by level to perform coloring in a linear sweep.
+          PDD nodes that are equal to 0 using some equality are marked as definitions.
+          First walk definitions to search for vanishing polynomial pairs. 
+          Given two definition polynomials d1, d2, it must be the case that 
+          level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing.        
+          Then starting from the lowest level examine pdd nodes. 
+          Let the current node be called p, check if the pdd node p is used in an equation
+          w - r = 0. In which case, w inherits the labels from r.
+          Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p).
+
+       Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2];
+       - Only apply GB saturation with respect to variables that are part of multipliers.
+       - Perhaps this amounts to figuring out whether a variable is used in an xor or more
+       
+    */
+
+    grobner::grobner(reslimit& lim, pdd_manager& m) : 
+        m(m),
+        m_limit(lim), 
+        m_conflict(nullptr)
+    {}
+
+    grobner::~grobner() {
+        reset();
+    }
+
+    void grobner::saturate() {
+        simplify();
+        if (is_tuned()) tuned_init();
+        TRACE("grobner", display(tout););
+        try {
+            while (!done() && step()) {
+                TRACE("grobner", display(tout););
+                DEBUG_CODE(invariant(););
+            }
+            DEBUG_CODE(invariant(););
+        }
+        catch (pdd_manager::mem_out) {
+            // don't reduce further
+        }
+    }
+
+    bool grobner::step() {
+        m_stats.m_compute_steps++;
+        return is_tuned() ? tuned_step() : basic_step();
+    }
+
+    bool grobner::basic_step() {
+        return basic_step(pick_next());
+    }
+
+    grobner::scoped_process::~scoped_process() {
+        if (e) {
+            pdd p = e->poly();
+            SASSERT(!p.is_val());
+            if (p.hi().is_val()) {
+                g.push_equation(solved, e);
+            }
+            else {
+                g.push_equation(processed, e);
+            }
+        }
+    }
+
+    bool grobner::basic_step(equation* e) {
+        if (!e) return false;
+        scoped_process sd(*this, e);
+        equation& eq = *e;
+        TRACE("grobner", display(tout << "eq = ", eq); display(tout););
+        SASSERT(eq.state() == to_simplify);
+        if (!simplify_using(eq, m_processed)) return false;
+        if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
+        if (check_conflict(eq)) { sd.e = nullptr; return false; }
+        if (!simplify_using(m_processed, eq)) return false;
+        superpose(eq);
+        return simplify_using(m_to_simplify, eq);
+    }
+    
+    grobner::equation* grobner::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 grobner::simplify() {
+        try {
+            while (!done() &&
+                   (simplify_linear_step(true) || 
+                    simplify_elim_pure_step() ||
+                    simplify_cc_step() || 
+                    simplify_leaf_step() ||
+                    simplify_linear_step(false) || 
+                    /*simplify_elim_dual_step() ||*/
+                    false)) {
+                DEBUG_CODE(invariant(););
+                TRACE("grobner", display(tout););
+            }
+        }
+        catch (pdd_manager::mem_out) {
+            // done reduce
+        }
+    }
+
+    struct grobner::compare_top_var {
+        bool operator()(equation* a, equation* b) const {
+            return a->poly().var() < b->poly().var();
+        }
+    };
+
+    bool grobner::simplify_linear_step(bool binary) {
+        TRACE("grobner", tout << "binary " << binary << "\n";);
+        equation_vector linear;
+        for (equation* e : m_to_simplify) {
+            pdd p = e->poly();
+            if (binary) {
+                if (p.is_binary()) linear.push_back(e);
+            }
+            else if (p.is_linear()) {
+                linear.push_back(e);
+            }
+        }
+        return simplify_linear_step(linear);
+    }
+
+    /**
+       \brief simplify linear equations by using top variable as solution.
+       The linear equation is moved to set of solved equations.
+    */
+    bool grobner::simplify_linear_step(equation_vector& linear) {
+        if (linear.empty()) return false;
+        use_list_t use_list = get_use_list();
+        compare_top_var ctv;
+        std::stable_sort(linear.begin(), linear.end(), ctv);
+        equation_vector trivial;
+        unsigned j = 0;
+        for (equation* src : linear) {
+            unsigned v = src->poly().var();
+            equation_vector const& uses = use_list[v];
+            TRACE("grobner", 
+                  display(tout << "uses of: ", *src) << "\n";
+                  for (equation* e : uses) {
+                      display(tout, *e) << "\n";
+                  });
+            bool changed_leading_term;
+            bool all_reduced = true;
+            for (equation* dst : uses) {
+                if (src == dst || is_trivial(*dst)) {
+                    continue;                    
+                }
+                pdd q = dst->poly();
+                if (!src->poly().is_binary() && !q.is_linear()) {
+                    all_reduced = false;
+                    continue;
+                }
+                remove_from_use(dst, use_list, v);
+                simplify_using(*dst, *src, changed_leading_term);
+                if (is_trivial(*dst)) {
+                    trivial.push_back(dst);
+                }
+                else if (is_conflict(dst)) {
+                    pop_equation(dst);
+                    set_conflict(dst);
+                    return true;
+                }
+                else if (changed_leading_term) {
+                    pop_equation(dst);
+                    push_equation(to_simplify, dst);
+                }
+                // v has been eliminated.
+                SASSERT(!m.free_vars(dst->poly()).contains(v));
+                add_to_use(dst, use_list);                
+            }          
+            if (all_reduced) {
+                linear[j++] = src;              
+            }
+        }
+        linear.shrink(j);      
+        for (equation* src : linear) {
+            pop_equation(src);
+            push_equation(solved, src);
+        }
+        for (equation* e : trivial) {
+            del_equation(e);
+        }
+        DEBUG_CODE(invariant(););
+        return j > 0;
+    }
+
+    /**
+       \brief simplify using congruences
+       replace pair px + q and ry + q by
+       px + q, px - ry
+       since px = ry
+     */
+    bool grobner::simplify_cc_step() {
+        TRACE("grobner", tout << "cc\n";);
+        u_map<equation*> los;
+        bool reduced = false;
+        unsigned j = 0;
+        for (equation* eq1 : m_to_simplify) {
+            SASSERT(eq1->state() == to_simplify);
+            pdd p = eq1->poly();
+            auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
+            equation* eq2 = e->get_data().m_value;
+            pdd q = eq2->poly();
+            if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) {
+                *eq1 = p - eq2->poly();
+                *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
+                reduced = true;
+                if (is_trivial(*eq1)) {
+                    retire(eq1);
+                    continue;
+                }
+                else if (check_conflict(*eq1)) {
+                    continue;
+                }
+            }
+            m_to_simplify[j] = eq1;
+            eq1->set_index(j++);
+        }
+        m_to_simplify.shrink(j);
+        return reduced;
+    }
+
+    /**
+       \brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
+    */
+    bool grobner::simplify_leaf_step() {
+        TRACE("grobner", tout << "leaf\n";);
+        use_list_t use_list = get_use_list();
+        equation_vector leaves;
+        for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
+            equation* e = m_to_simplify[i];
+            pdd p = e->poly();
+            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 : leaves) {
+                bool changed_leading_term;
+                remove_from_use(e2, use_list);
+                simplify_using(*e2, *e, changed_leading_term);
+                add_to_use(e2, use_list);
+                if (is_trivial(*e2)) {
+                    pop_equation(e2);
+                    retire(e2);
+                }
+                else if (e2->poly().is_val()) {
+                    pop_equation(e2);
+                    set_conflict(*e2);
+                    return true;
+                }
+                else if (changed_leading_term) {
+                    pop_equation(e2);
+                    push_equation(to_simplify, e2);
+                }
+            }
+        }
+        return false;
+    }
+
+    /**
+       \brief treat equations as processed if top variable occurs only once.
+    */
+    bool grobner::simplify_elim_pure_step() {
+        TRACE("grobner", tout << "pure\n";);
+        use_list_t use_list = get_use_list();        
+        unsigned j = 0;
+        for (equation* e : m_to_simplify) {
+            pdd p = e->poly();
+            if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
+                push_equation(solved, e);
+            }
+            else {
+                m_to_simplify[j] = e;
+                e->set_index(j++);
+            }
+        }
+        if (j != m_to_simplify.size()) {
+            m_to_simplify.shrink(j);
+            return true;
+        }
+        return false;
+    }
+
+    /**
+       \brief 
+       reduce equations where top variable occurs only twice and linear in one of the occurrences.       
+     */
+    bool grobner::simplify_elim_dual_step() {
+        use_list_t use_list = get_use_list();        
+        unsigned j = 0;
+        bool reduced = false;
+        for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
+            equation* e = m_to_simplify[i];            
+            pdd p = e->poly();
+            // check that e is linear in top variable.
+            if (e->state() != to_simplify) {
+                reduced = true;
+            }
+            else if (!done() && !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);
+                    simplify_using(*e2, *e, changed_leading_term);
+                    if (is_conflict(e2)) {
+                        pop_equation(e2);
+                        set_conflict(e2);
+                    }
+                    // when e2 is trivial, leading term is changed
+                    SASSERT(!is_trivial(*e2) || changed_leading_term);
+                    if (changed_leading_term) {
+                        pop_equation(e2);
+                        push_equation(to_simplify, e2);
+                    }
+                    add_to_use(e2, use_list);
+                    break;
+                }
+                reduced = true;
+                push_equation(solved, e);
+            }
+            else {
+                m_to_simplify[j] = e;
+                e->set_index(j++);
+            }
+        }
+        if (reduced) {
+            // clean up elements in m_to_simplify 
+            // they may have moved.
+            m_to_simplify.shrink(j);
+            j = 0;
+            for (equation* e : m_to_simplify) {
+                if (is_trivial(*e)) {
+                    retire(e);
+                }
+                else if (e->state() == to_simplify) {
+                    m_to_simplify[j] = e;
+                    e->set_index(j++);
+                }
+            }
+            m_to_simplify.shrink(j);
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
+    void grobner::add_to_use(equation* e, use_list_t& use_list) {
+        unsigned_vector const& fv = m.free_vars(e->poly());
+        for (unsigned v : fv) {
+            use_list.reserve(v + 1);
+            use_list[v].push_back(e);
+        }
+    }
+
+    void grobner::remove_from_use(equation* e, use_list_t& use_list) {
+        unsigned_vector const& fv = m.free_vars(e->poly());
+        for (unsigned v : fv) {
+            use_list.reserve(v + 1);
+            use_list[v].erase(e);
+        }
+    }
+
+    void grobner::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) {
+        unsigned_vector const& fv = m.free_vars(e->poly());
+        for (unsigned v : fv) {
+            if (v != except_v) {
+                use_list.reserve(v + 1);
+                use_list[v].erase(e);
+            }
+        }
+    }
+
+    grobner::use_list_t grobner::get_use_list() {
+        use_list_t use_list;
+        for (equation * e : m_to_simplify) {
+            add_to_use(e, use_list);
+        }
+        for (equation * e : m_processed) {
+            add_to_use(e, use_list);
+        }
+        return use_list;
+    }
+
+    void grobner::superpose(equation const & eq) {
+        for (equation* target : m_processed) {
+            superpose(eq, *target);
+        }
+    }
+
+    /*
+      Use a set of equations to simplify eq
+    */
+    bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
+        bool simplified, changed_leading_term;
+        do {
+            simplified = false;
+            for (equation* p : eqs) {
+                if (try_simplify_using(eq, *p, changed_leading_term)) {
+                    simplified = true;
+                }
+                if (canceled() || eq.poly().is_val()) {
+                    break;
+                }
+            }
+        }
+        while (simplified && !eq.poly().is_val());
+
+        TRACE("grobner", display(tout << "simplification result: ", eq););
+
+        return !done();
+    }
+
+    /*
+      Use the given equation to simplify equations in set
+    */
+    bool grobner::simplify_using(equation_vector& set, equation const& eq) {
+        unsigned j = 0, sz = set.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            equation& target = *set[i];
+            bool changed_leading_term = false;
+            bool simplified = !done() && try_simplify_using(target, eq, changed_leading_term); 
+            if (simplified && is_trivial(target)) {
+                retire(&target);
+            }
+            else if (simplified && check_conflict(target)) {
+                // pushed to solved
+            }
+            else if (simplified && changed_leading_term) {
+                SASSERT(target.state() == processed);
+                push_equation(to_simplify, target);
+                if (!m_watch.empty()) {
+                    m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
+                    add_to_watch(target);
+                }
+            }
+            else {
+                set[j] = set[i];
+                target.set_index(j++);                
+            } 
+        }
+        set.shrink(j);
+        return !done();
+    }    
+
+    /*
+      simplify target using source.
+      return true if the target was simplified. 
+      set changed_leading_term if the target is in the m_processed set and the leading term changed.
+     */
+    bool grobner::try_simplify_using(equation& dst, equation const& src, bool& changed_leading_term) {
+        if (&src == &dst) {
+            return false;
+        }
+        m_stats.m_simplified++;
+        pdd t = src.poly();
+        pdd r = dst.poly().reduce(t);
+        if (r == dst.poly() || is_too_complex(r)) {
+            return false;
+        }
+        TRACE("grobner", 
+              tout << "reduce: " << dst.poly() << "\n";
+              tout << "using:  " << t << "\n";
+              tout << "to:     " << r << "\n";);
+        changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
+        dst = r;
+        dst = m_dep_manager.mk_join(dst.dep(), src.dep());
+        update_stats_max_degree_and_size(dst);
+        return true;
+    }
+
+    void grobner::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) {
+        if (&src == &dst) return;        
+        m_stats.m_simplified++;
+        pdd t = src.poly();
+        pdd r = dst.poly().reduce(t);
+        changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
+        TRACE("grobner", 
+              tout << "reduce: " << dst.poly() << "\n";
+              tout << "using:  " << t << "\n";
+              tout << "to:     " << r << "\n";);
+
+        if (r == dst.poly()) return;
+        dst = r;
+        dst = m_dep_manager.mk_join(dst.dep(), src.dep());
+        update_stats_max_degree_and_size(dst);
+    }
+
+    /*
+       let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
+    */
+    void grobner::superpose(equation const& eq1, equation const& eq2) {
+        TRACE("grobner_d", display(tout << "eq1=", eq1); display(tout << "eq2=", eq2););
+        pdd r(m);
+        if (m.try_spoly(eq1.poly(), eq2.poly(), r) && 
+            !r.is_zero() && !is_too_complex(r)) {
+            m_stats.m_superposed++;
+            add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
+        }
+    }
+
+    bool grobner::tuned_step() {
+        equation* e = tuned_pick_next();
+        if (!e) return false;
+        scoped_process sd(*this, e);
+        equation& eq = *e;
+        SASSERT(!m_watch[eq.poly().var()].contains(e));
+        SASSERT(eq.state() == to_simplify);
+        if (!simplify_using(eq, m_processed)) return false;
+        if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
+        if (check_conflict(eq)) { sd.e = nullptr; return false; }
+        if (!simplify_using(m_processed, eq)) return false;
+        TRACE("grobner", display(tout << "eq = ", eq););
+        superpose(eq);
+        simplify_watch(eq);
+        return true;
+    }
+
+    void grobner::tuned_init() {
+        unsigned_vector const& l2v = m.get_level2var();
+        m_level2var.resize(l2v.size());
+        m_var2level.resize(l2v.size());
+        for (unsigned i = 0; i < l2v.size(); ++i) {
+            m_level2var[i] = l2v[i];
+            m_var2level[l2v[i]] = i;
+        }
+        m_watch.reset();
+        m_watch.reserve(m_level2var.size());
+        m_levelp1 = m_level2var.size();
+        for (equation* eq : m_to_simplify) add_to_watch(*eq);
+    }
+
+    void grobner::add_to_watch(equation& eq) {
+        SASSERT(eq.state() == to_simplify);
+        SASSERT(is_tuned());
+        pdd const& p = eq.poly();
+        if (!p.is_val()) {
+            m_watch[p.var()].push_back(&eq);
+        }
+    }
+
+    void grobner::simplify_watch(equation const& eq) {
+        unsigned v = eq.poly().var();
+        auto& watch = m_watch[v];
+        unsigned j = 0;
+        for (equation* _target : watch) {
+            equation& target = *_target;
+            SASSERT(target.state() == to_simplify);
+            SASSERT(target.poly().var() == v);
+            bool changed_leading_term = false;
+            if (!done()) {
+                try_simplify_using(target, eq, changed_leading_term);
+            }
+            if (is_trivial(target)) {
+                pop_equation(target);
+                retire(&target);
+            }
+            else if (is_conflict(target)) {
+                pop_equation(target);
+                set_conflict(target);
+            }
+            else if (target.poly().var() != v) {
+                // move to other watch list
+                m_watch[target.poly().var()].push_back(_target);
+            }
+            else {
+                // keep watching same variable
+                watch[j++] = _target;
+            }
+        }
+        watch.shrink(j);        
+    }
+
+    grobner::equation* grobner::tuned_pick_next() {
+        while (m_levelp1 > 0) {
+            unsigned v = m_level2var[m_levelp1-1];
+            equation_vector const& watch = m_watch[v];
+            equation* eq = nullptr;
+            for (equation* curr : watch) {
+                pdd const& p = curr->poly();
+                if (curr->state() == to_simplify && p.var() == v) {
+                    if (!eq || is_simpler(*curr, *eq))
+                        eq = curr;
+                }
+            }
+            if (eq) {
+                pop_equation(eq);
+                m_watch[eq->poly().var()].erase(eq);
+                return eq;
+            }
+            --m_levelp1;
+        }
+        return nullptr;
+    }
+
+    grobner::equation_vector const& grobner::equations() {
+        m_all_eqs.reset();
+        for (equation* eq : m_solved) m_all_eqs.push_back(eq);
+        for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq);
+        for (equation* eq : m_processed) m_all_eqs.push_back(eq);
+        return m_all_eqs;
+    }
+
+    void grobner::reset() {
+        for (equation* e : m_solved) dealloc(e);
+        for (equation* e : m_to_simplify) dealloc(e);
+        for (equation* e : m_processed) dealloc(e);
+        m_solved.reset();
+        m_processed.reset();
+        m_to_simplify.reset();
+        m_stats.reset();
+        m_watch.reset();
+        m_level2var.reset();
+        m_var2level.reset();
+        m_conflict = nullptr;
+    }
+
+    void grobner::add(pdd const& p, u_dependency * dep) {
+        if (p.is_zero()) return;
+        equation * eq = alloc(equation, p, dep);
+        if (check_conflict(*eq)) {
+            return;
+        }
+        push_equation(to_simplify, eq);
+        
+        if (!m_watch.empty()) {
+            m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
+            add_to_watch(*eq);
+        }
+        update_stats_max_degree_and_size(*eq);
+    }   
+    
+    bool grobner::canceled() {
+        return m_limit.get_cancel_flag();
+    }
+    
+    bool grobner::done() {
+        return 
+            m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || 
+            canceled() || 
+            m_conflict != nullptr;
+    }
+
+    grobner::equation_vector& grobner::get_queue(equation const& eq) {
+        switch (eq.state()) {
+        case processed: return m_processed;
+        case to_simplify: return m_to_simplify;
+        case solved: return m_solved;
+        }
+        UNREACHABLE();
+        return m_to_simplify;
+    }
+
+    void grobner::del_equation(equation* eq) {
+        pop_equation(eq);
+        retire(eq);
+    }
+
+    void grobner::pop_equation(equation& eq) {
+        equation_vector& v = get_queue(eq);
+        unsigned idx = eq.idx();
+        if (idx != v.size() - 1) {
+            equation* eq2 = v.back();
+            eq2->set_index(idx);
+            v[idx] = eq2;
+        }
+        v.pop_back();            
+    }
+
+    void grobner::push_equation(eq_state st, equation& eq) {
+        eq.set_state(st);
+        equation_vector& v = get_queue(eq);
+        eq.set_index(v.size());
+        v.push_back(&eq);
+    }
+    
+    void grobner::update_stats_max_degree_and_size(const equation& e) {
+        m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size());
+        m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly().degree());
+    }
+    
+    void grobner::collect_statistics(statistics& st) const {
+        st.update("steps", m_stats.m_compute_steps);
+        st.update("simplified", m_stats.m_simplified);
+        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);
+    }
+            
+    std::ostream& grobner::display(std::ostream & out, const equation & eq) const {
+        out << eq.poly() << "\n";
+        if (m_print_dep) m_print_dep(eq.dep(), out);
+        return out;
+    }
+
+    std::ostream& grobner::display(std::ostream& out) const {
+        out << "solved\n"; for (auto e : m_solved) display(out, *e);
+        out << "processed\n"; for (auto e : m_processed) display(out, *e);
+        out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
+        statistics st;
+        collect_statistics(st);
+        st.display(out);
+        return out;
+    }
+
+    void grobner::invariant() const {
+        // equations in processed have correct indices
+        // they are labled as processed
+        unsigned i = 0;
+        for (auto* e : m_processed) {
+            VERIFY(e->state() == processed);
+            VERIFY(e->idx() == i);
+            VERIFY(!e->poly().is_val());
+            ++i;
+        }
+
+        i = 0;
+        uint_set head_vars;
+        for (auto* e : m_solved) {
+            VERIFY(e->state() == solved);
+            VERIFY(e->idx() == i);
+            ++i;
+            pdd p = e->poly();
+            if (!p.is_val() && p.hi().is_val()) {
+                unsigned v = p.var();
+                SASSERT(!head_vars.contains(v));
+                head_vars.insert(v);
+            }
+        }
+
+        if (!head_vars.empty()) {
+            for (auto * e : m_to_simplify) {
+                for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
+            }
+            for (auto * e : m_processed) {
+                for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
+            }
+        }
+
+        // equations in to_simplify have correct indices
+        // they are labeled as non-processed
+        // their top-most variable is watched
+        i = 0;
+        for (auto* e : m_to_simplify) {
+            VERIFY(e->idx() == i);
+            VERIFY(e->state() == to_simplify);
+            pdd const& p = e->poly();
+            VERIFY(!p.is_val());
+            CTRACE("grobner", !m_watch.empty() && !m_watch[p.var()].contains(e), 
+                   display(tout << "not watched: ", *e) << "\n";);
+            VERIFY(m_watch.empty() || m_watch[p.var()].contains(e));            
+            ++i;
+        }
+        // the watch list consists of equations in to_simplify
+        // they watch the top most variable in poly
+        i = 0;
+        for (auto const& w : m_watch) {            
+            for (equation* e : w) {
+                VERIFY(!e->poly().is_val());
+                VERIFY(e->poly().var() == i);
+                VERIFY(e->state() == to_simplify);
+                VERIFY(m_to_simplify.contains(e));
+            }
+            ++i;
+        }
+    }
+}
+
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 10345ee58..9174bded0 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -486,7 +486,7 @@ interv intervals::interval_of_expr(const nex* e, unsigned p) {
         return b;
     }
     case expr_type::MUL: {
-        interv b = interval_of_mul<with_deps>(e->to_mul());
+        interv b = interval_of_mul<wd>(e->to_mul());
         if (p != 1)
             return power<wd>(b, p);
         return b;
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index ba55309e0..5f3e89823 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -135,7 +135,6 @@ class intervals {
     };
 
     region                              m_alloc;
-    common::ci_value_manager            m_val_manager;
     mutable unsynch_mpq_manager         m_num_manager;
     mutable u_dependency_manager        m_dep_manager;
     im_config                           m_config;