diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 7d9b3efa2..8c3269435 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -366,7 +366,7 @@ namespace dd {
     // since x is the maximal variable, it does not occur in t or v.
     // thus, both a and b are linear in x
     bool pdd_manager::spoly_is_invertible(pdd const& a, pdd const& b) {
-        return a.is_var() && b.is_var() && a.hi().is_val() && b.hi().is_val() && a.var() == b.var();
+        return !a.is_val() && !b.is_val() && a.hi().is_val() && b.hi().is_val() && a.var() == b.var();
     }
 
     /*
@@ -617,22 +617,8 @@ namespace dd {
     }
 
     unsigned_vector const& pdd_manager::free_vars(pdd const& p) { 
-        return free_vars_except(p, zero()); 
-    }
-
-    unsigned_vector const& pdd_manager::free_vars_except(pdd const& p, pdd const& q) {
         init_mark();
         m_free_vars.reset();
-        m_todo.push_back(q.root);
-        while (!m_todo.empty()) {
-            PDD r = m_todo.back();
-            m_todo.pop_back();
-            if (is_val(r) || is_marked(r)) continue;            
-            set_mark(r);            
-            set_mark(m_var2pdd[var(r)]);            
-            if (!is_marked(lo(r))) m_todo.push_back(lo(r));
-            if (!is_marked(hi(r))) m_todo.push_back(hi(r));
-        }
         m_todo.push_back(p.root);
         while (!m_todo.empty()) {
             PDD r = m_todo.back();
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 5de035c11..3ac44d974 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -246,7 +246,6 @@ namespace dd {
         double tree_size(pdd const& p);
 
         unsigned_vector const& free_vars(pdd const& p);
-        unsigned_vector const& free_vars_except(pdd const& p, pdd const& q);
 
         std::ostream& display(std::ostream& out);
         std::ostream& display(std::ostream& out, pdd const& b);
@@ -269,7 +268,6 @@ namespace dd {
         pdd hi() const { return pdd(m->hi(root), m); }
         unsigned var() const { return m->var(root); }
         rational const& val() const { SASSERT(is_val()); return m->val(root); }
-        bool is_var() const { return !m->is_val(root); }
         bool is_val() const { return m->is_val(root); }
         bool is_zero() const { return m->is_zero(root); }
 
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index 970fa14e8..a0fa7edd4 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -55,7 +55,7 @@ namespace dd {
         For p in A:
             populate watch list by maxvar(p) |-> p
         For p in S:
-            populate watch list by vars(p) |-> p
+            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
@@ -69,7 +69,7 @@ namespace dd {
         The alternative version maintains the following invariant:
         - polynomials not in the watch list cannot be simplified using a
           Justification:
-          - elements in S have all variables watched
+          - elements in S have no variables watched
           - elements in A are always reduced modulo all variables above the current x_i.
 
         Invertible rules:
@@ -106,12 +106,7 @@ namespace dd {
 
     bool grobner::step() {
         m_stats.m_compute_steps++;
-        if (is_tuned()) {
-            return tuned_step();
-        }
-        else {
-            return basic_step();
-        }
+        return is_tuned() ? tuned_step() : basic_step();
     }
 
     bool grobner::basic_step() {
@@ -226,20 +221,6 @@ namespace dd {
         if (changed_leading_term) {
             target.set_processed(false);
         }
-        if (is_tuned()) {
-            if (r == t) {
-                // noop
-            }
-            else if (changed_leading_term) {
-                add_to_watch(target);
-            }
-            else if (target.is_processed()) {
-                add_diff_to_watch(target, t);
-            }
-            else {
-                add_to_watch(target);
-            }            
-        }
 
         TRACE("grobner", tout << "simplified " << target.poly() << "\n";);
         return true;
@@ -262,8 +243,9 @@ namespace dd {
         equation* e = tuned_pick_next();
         if (!e) return false;
         equation& eq = *e;
+        SASSERT(!m_watch[eq.poly().var()].contains(e));
         SASSERT(!eq.is_processed());
-        if (!simplify_watch(eq, true)) return false;
+        if (!simplify_using(eq, m_processed)) return false;
         if (eliminate(eq)) return true;
         if (check_conflict(eq)) return false;
         if (!simplify_using(m_processed, eq)) return false;
@@ -271,8 +253,7 @@ namespace dd {
         superpose(eq);
         eq.set_processed(true);
         m_processed.push_back(e);
-        add_diff_to_watch(eq, m.zero());
-        return simplify_watch(eq, false);
+        return simplify_to_simplify(eq);
     }
 
     void grobner::tuned_init() {
@@ -292,23 +273,13 @@ namespace dd {
         }
     }
 
-    // add all variables in q but not p into watch.
-    void grobner::add_diff_to_watch(equation& eq, pdd const& p) {
-        SASSERT(eq.is_processed());
-        pdd const& q = eq.poly();
-        if (is_tuned() && !q.is_val()) {
-            for (unsigned v : m.free_vars_except(q, p)) {
-                m_watch[v].push_back(&eq);
-            }
-        }
-    }
-
-    bool grobner::simplify_watch(equation const& eq, bool is_processed) {
+    bool grobner::simplify_to_simplify(equation const& eq) {
         unsigned v = m_vars[m_var];
         auto& watch = m_watch[v];
         unsigned j = 0;
         for (equation* _target : watch) {
             equation& target = *_target;
+            if (target.is_processed()) continue;
             bool changed_leading_term = false;
             bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
             if (simplified && is_trivial(target)) {
@@ -341,6 +312,7 @@ namespace dd {
             }
             if (eq) {
                 pop_equation(eq->idx(), m_to_simplify);
+                m_watch[eq->poly().var()].erase(eq);
                 return eq;
             }
             ++m_var;
@@ -428,16 +400,37 @@ namespace dd {
     }
 
     void grobner::invariant() const {
+        // equations in processed have correct indices
+        // they are labled as processed
         unsigned i = 0;
         for (auto* e : m_processed) {
-            SASSERT(e->is_processed());            
-            SASSERT(e->idx() == i);
+            VERIFY(e->is_processed());            
+            VERIFY(e->idx() == i);
             ++i;
         }
+        // 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) {
-            SASSERT(!e->is_processed());            
-            SASSERT(e->idx() == i);
+            VERIFY(!e->is_processed());            
+            VERIFY(e->idx() == i);
+            if (is_tuned()) {
+                pdd const& p = e->poly();
+                VERIFY(p.is_val() || 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 const* e : w) {
+                VERIFY(!e->poly().is_val());
+                VERIFY(e->poly().var() == i);
+                VERIFY(!e->is_processed());
+                VERIFY(m_to_simplify.contains(e));
+            }
             ++i;
         }
     }
diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h
index f2690c38f..5ece8560e 100644
--- a/src/math/grobner/pdd_grobner.h
+++ b/src/math/grobner/pdd_grobner.h
@@ -135,14 +135,11 @@ private:
     bool tuned_step();
     void tuned_init();
     equation* tuned_pick_next();
-    bool simplify_watch(equation const& eq, bool is_processed);
+    bool simplify_to_simplify(equation const& eq);
     void add_to_watch(equation& eq);
-    void add_diff_to_watch(equation& eq, pdd const& p);
 
     void del_equation(equation& eq);    
     void retire(equation* eq) {
-        if (is_tuned())
-            for (auto v : m.free_vars(eq->poly())) m_watch[v].erase(eq);
         dealloc(eq);
     }
     void pop_equation(unsigned idx, equation_vector& v);
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 77d2fe248..2e102f4e4 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1080,7 +1080,6 @@ namespace qe {
             return true;
         }
 
-
         bool is_unit() const { 
             return m_children.size() == 1 && 
                    m_branch_index.empty(); 
@@ -1430,7 +1429,7 @@ namespace qe {
             // set sub-formula
             m_fml = fml;
             normalize(m_fml, m_root.pos_atoms(), m_root.neg_atoms());
-            expr_ref f(m_fml);           
+            expr_ref f(m_fml);
             get_max_relevant(get_is_relevant(), f, m_subfml);
             if (f.get() != m_subfml.get()) {
                 m_fml = f;
@@ -1465,6 +1464,11 @@ namespace qe {
 
             if (!is_sat) {
                 fml = m.mk_false();
+                if (m_fml.get() != m_subfml.get()) {
+                    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m);
+                    rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
+                    fml = m_fml;
+                }
                 reset();
                 m_solver.pop(1);
                 return;
@@ -2227,7 +2231,9 @@ namespace qe {
     }
 
     void expr_quant_elim::operator()(expr* assumption, expr* fml, expr_ref& result) {
-        TRACE("qe", tout << "elim input\n"  << mk_ismt2_pp(fml, m) << "\n";);
+        TRACE("qe", 
+              if (assumption) tout << "elim assumption\n" << mk_ismt2_pp(assumption, m) << "\n";
+              tout << "elim input\n"  << mk_ismt2_pp(fml, m) << "\n";);
         expr_ref_vector bound(m);
         result = fml;
         m_assumption = assumption;
@@ -2312,14 +2318,13 @@ namespace qe {
             case AST_APP: {
                 app* a = to_app(e);
                 expr_ref_vector args(m);
-                unsigned num_args = a->get_num_args();
                 bool all_visited = true;
-                for (unsigned i = 0; i < num_args; ++i) {
-                    if (m_visited.find(a->get_arg(i), r)) {
+                for (expr* arg : *a) {
+                    if (m_visited.find(arg, r)) {
                         args.push_back(r);
                     }
                     else {
-                        todo.push_back(a->get_arg(i));
+                        todo.push_back(arg);
                         all_visited = false;
                     }
                 }