diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 14fc0dcce..13451f270 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -27,6 +27,7 @@ namespace dd {
         m_spare_entry = nullptr;
         m_max_num_nodes = 1 << 24; // up to 16M nodes
         m_mark_level = 0;
+        m_dmark_level = 0;
         m_disable_gc = false;
         m_is_new_node = false;
         m_semantics = s;
@@ -398,15 +399,18 @@ namespace dd {
 
     // true if leading monomial of p divides leading monomial of q
     bool pdd_manager::lm_divides(PDD p, PDD q) const {
+        p = first_leading(p);
+        q = first_leading(q);
         while (true) {
             if (is_val(p)) return true;
             if (is_val(q)) return false;
             if (level(p) > level(q)) return false;
             if (level(p) == level(q)) {
-                p = hi(p); q = hi(q);
+                p = next_leading(p);
+                q = next_leading(q);
             }
             else {
-                q = hi(q);
+                q = next_leading(q);
             }
         }
     }
@@ -415,6 +419,8 @@ namespace dd {
     // assume lm_divides(p, q)
     pdd_manager::PDD pdd_manager::lt_quotient(PDD p, PDD q) {
         SASSERT(lm_divides(p, q));
+        p = first_leading(p);
+        q = first_leading(q);
         SASSERT(is_val(p) || !is_val(q));
         if (is_val(p)) {
             if (is_val(q)) {
@@ -423,12 +429,15 @@ namespace dd {
             }
         }
         else if (level(p) == level(q)) {
-            return lt_quotient(hi(p), hi(q));
+            return lt_quotient(next_leading(p), next_leading(q));
         }
-        push(lt_quotient(p, hi(q)));
+
+        SASSERT(!is_val(q));
+        push(lt_quotient(p, next_leading(q)));
         PDD r = apply_rec(m_var2pdd[var(q)], read(1), pdd_mul_op);
         pop(1);
-        return r;                   
+        return r;  
+                         
     }
 
     //
@@ -450,13 +459,13 @@ namespace dd {
 
     bool pdd_manager::common_factors(pdd const& a, pdd const& b, unsigned_vector& p, unsigned_vector& q, rational& pc, rational& qc) { 
         p.reset(); q.reset(); 
-        PDD x = a.root, y = b.root;
+        PDD x = first_leading(a.root), y = first_leading(b.root);
         bool has_common = false;
         while (true) {
             if (is_val(x) || is_val(y)) {
                 if (!has_common) return false;
-                while (!is_val(y)) q.push_back(var(y)), y = hi(y);
-                while (!is_val(x)) p.push_back(var(x)), x = hi(x);
+                while (!is_val(y)) q.push_back(var(y)), y = next_leading(y);
+                while (!is_val(x)) p.push_back(var(x)), x = next_leading(x);
                 pc = val(x);
                 qc = val(y);
                 if (m_semantics != mod2_e && pc.is_int() && qc.is_int()) {
@@ -468,24 +477,25 @@ namespace dd {
             }
             if (level(x) == level(y)) {
                 has_common = true;
-                x = hi(x);
-                y = hi(y);
+                x = next_leading(x);
+                y = next_leading(y);
             }
             else if (level(x) > level(y)) {
                 p.push_back(var(x));
-                x = hi(x);
+                x = next_leading(x);
             }
             else {
                 q.push_back(var(y));
-                y = hi(y);
+                y = next_leading(y);
             }
         }
     }
 
-    /*
-     * Compare leading monomials.
+    /*.
      * The pdd format makes lexicographic comparison easy: compare based on
      * the top variable and descend depending on whether hi(x) == hi(y)
+     *
+     * NB. this does not compare leading monomials.
      */
     bool pdd_manager::lt(pdd const& a, pdd const& b) {
         PDD x = a.root;
@@ -517,14 +527,14 @@ namespace dd {
        Compare leading terms of pdds
      */
     bool pdd_manager::different_leading_term(pdd const& a, pdd const& b) {
-        PDD x = a.root;
-        PDD y = b.root;
+        PDD x = first_leading(a.root);
+        PDD y = first_leading(b.root);
         while (true) {
             if (x == y) return false;
             if (is_val(x) || is_val(y)) return true;
             if (level(x) == level(y)) {
-                x = hi(x);
-                y = hi(y);
+                x = next_leading(x);
+                y = next_leading(y);
             }
             else {
                 return true;
@@ -532,6 +542,28 @@ namespace dd {
         }
     }
 
+    /**
+     * The assumption is that var(p) is part of the leading monomial.
+     * Then the next leading monomial that uses var(p) has to be under hi(p)
+     * because lo(p) does not use var(p).
+     */
+    pdd_manager::PDD pdd_manager::next_leading(PDD p) const {
+        SASSERT(!is_val(p));
+        return first_leading(hi(p));
+    }
+
+    /**
+     * The first node that contains a term from the leading monomial
+     * is a node of highest degree and highest variable.
+     * Thus, when the degree of hi(p) + 1 is not dominated by degree of lo(p).
+     */
+    pdd_manager::PDD pdd_manager::first_leading(PDD p) const {
+        while (!is_val(p) && degree(hi(p)) + 1 < degree(lo(p))) {
+            p = lo(p);
+        }
+        return p;
+    }
+
     /*
       Determine whether p is a linear polynomials.
       A linear polynomial is of the form x*v1 + y*v2 + .. + vn,
@@ -764,29 +796,44 @@ namespace dd {
         return sz;
     }
 
-    unsigned pdd_manager::degree(pdd const& b) {
-        init_mark();
+    void pdd_manager::init_dmark() {
+        m_dmark.resize(m_nodes.size());
         m_degree.reserve(m_nodes.size());
-        m_todo.push_back(b.root);
+        ++m_dmark_level;
+        if (m_dmark_level == 0) {
+            m_dmark.fill(0);
+            ++m_dmark_level;
+        }
+    }
+
+    unsigned pdd_manager::degree(pdd const& b) const {
+        return degree(b.root);
+    }
+
+    unsigned pdd_manager::degree(PDD p) const {
+        if (is_dmarked(p)) {
+            return m_degree[p];
+        }        
+        m_todo.push_back(p);
         while (!m_todo.empty()) {
             PDD r = m_todo.back();
-            if (is_marked(r)) {
+            if (is_dmarked(r)) {
                 m_todo.pop_back();
             }
             else if (is_val(r)) {
                 m_degree[r] = 0;
-                set_mark(r);
+                set_dmark(r);
             }
-            else if (!is_marked(lo(r)) || !is_marked(hi(r))) {
+            else if (!is_dmarked(lo(r)) || !is_dmarked(hi(r))) {
                 m_todo.push_back(lo(r));
                 m_todo.push_back(hi(r));
             }
             else {
                 m_degree[r] = std::max(m_degree[lo(r)], m_degree[hi(r)]+1); 
-                set_mark(r);
+                set_dmark(r);
             }
         }
-        return m_degree[b.root];
+        return m_degree[p];
     }
 
 
@@ -833,7 +880,6 @@ namespace dd {
         return m_free_vars;
     }
 
-
     void pdd_manager::alloc_free_nodes(unsigned n) {
         for (unsigned i = 0; i < n; ++i) {
             m_free_nodes.push_back(m_nodes.size());
@@ -842,6 +888,7 @@ namespace dd {
         }        
         std::sort(m_free_nodes.begin(), m_free_nodes.end());
         m_free_nodes.reverse();
+        init_dmark();
     }
 
     bool pdd_manager::is_reachable(PDD p) {
@@ -883,6 +930,7 @@ namespace dd {
     }
 
     void pdd_manager::gc() {
+        init_dmark();
         m_free_nodes.reset();
         SASSERT(well_formed());
         IF_VERBOSE(13, verbose_stream() << "(pdd :gc " << m_nodes.size() << ")\n";);
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 8da53d55d..1168952d4 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -213,7 +213,14 @@ namespace dd {
         inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
 
         unsigned dag_size(pdd const& p);
-        unsigned degree(pdd const& p);
+
+        mutable svector<unsigned>  m_dmark;
+        mutable unsigned           m_dmark_level;
+        void init_dmark();
+        void set_dmark(unsigned i) const { m_dmark[i] = m_dmark_level; }
+        bool is_dmarked(unsigned i) const { return m_dmark[i] == m_dmark_level; }
+        unsigned degree(pdd const& p) const;
+        unsigned degree(PDD p) const;
 
         bool var_is_leaf(PDD p, unsigned v);
 
@@ -228,6 +235,8 @@ namespace dd {
         rational m_pc, m_qc;
         pdd spoly(pdd const& a, pdd const& b, unsigned_vector const& p, unsigned_vector const& q, rational const& pc, rational const& qc);
         bool common_factors(pdd const& a, pdd const& b, unsigned_vector& p, unsigned_vector& q, rational& pc, rational& qc);
+        PDD first_leading(PDD p) const;
+        PDD next_leading(PDD p) const;
 
         monomials_t to_monomials(pdd const& p);