diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 90104a071..4d492d8fc 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -495,12 +495,9 @@ namespace dd {
     }
 
     /*.
-     * 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.
+     * compare pdds based on leading monomials
      */
-    bool pdd_manager::lt(pdd const& a, pdd const& b) {
+    bool pdd_manager::lex_lt(pdd const& a, pdd const& b) {
         PDD x = a.root;
         PDD y = b.root;
         if (x == y) return false;
@@ -526,6 +523,48 @@ namespace dd {
         }
     }
 
+    bool pdd_manager::lm_lt(pdd const& a, pdd const& b) {
+        PDD x = first_leading(a.root);
+        PDD y = first_leading(b.root);
+        while (true) {
+            if (x == y) break;
+            if (is_val(x) && is_val(y)) break;
+            if (is_val(x)) return true;
+            if (is_val(y)) return false;
+            if (level(x) == level(y)) {
+                x = next_leading(x);
+                y = next_leading(y);
+            }
+            else {
+                return level(x) < level(y);
+            }
+        }
+        vector<unsigned_vector> ma, mb;
+        for (auto const& m : a) {
+            ma.push_back(m.vars);
+        }
+        for (auto const& m : b) {
+            mb.push_back(m.vars);
+        }
+        std::function<bool (unsigned_vector const& a, unsigned_vector const& b)> degree_lex_gt = 
+            [this](unsigned_vector const& a, unsigned_vector const& b) {
+            unsigned i = 0;
+            if (a.size() > b.size()) return true;
+            if (a.size() < b.size()) return false;
+            for (; i < a.size() && a[i] == b[i]; ++i) {};
+            return i < a.size() && m_var2level[a[i]] > m_var2level[b[i]];
+        };
+        std::sort(ma.begin(), ma.end(), degree_lex_gt);
+        std::sort(mb.begin(), mb.end(), degree_lex_gt);
+        auto ita = ma.begin();
+        auto itb = mb.begin();
+        for (; ita != ma.end() && itb != mb.end(); ++ita, ++itb) {
+            if (degree_lex_gt(*itb, *ita)) return true;
+            if (degree_lex_gt(*ita, *itb)) return false;
+        }
+        return ita == ma.end() && itb != mb.end();
+    }
+
     /**
        Compare leading terms of pdds
      */
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index fbe35ade5..fe9b0ecf9 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -290,7 +290,12 @@ namespace dd {
         // create an spoly r if leading monomials of a and b overlap
         bool try_spoly(pdd const& a, pdd const& b, pdd& r);
 
-        bool lt(pdd const& a, pdd const& b);
+        // simple lexicographic comparison
+        bool lex_lt(pdd const& a, pdd const& b); 
+
+        // more elaborate comparison based on leading monomials
+        bool lm_lt(pdd const& a, pdd const& b);
+
         bool different_leading_term(pdd const& a, pdd const& b);
         double tree_size(pdd const& p);
         unsigned num_vars() const { return m_var2pdd.size(); }
@@ -352,9 +357,6 @@ namespace dd {
         std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
         bool operator==(pdd const& other) const { return root == other.root; }
         bool operator!=(pdd const& other) const { return root != other.root; }
-        bool operator<(pdd const& other) const { return m.lt(*this, other); }
-
-
 
         unsigned dag_size() const { return m.dag_size(*this); }
         double tree_size() const { return m.tree_size(*this); }
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 56e71570a..671bd94b0 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -70,9 +70,11 @@ namespace dd {
     }
 
 
-// some of the config fields are set, others are calculated
     void solver::set_thresholds() {
         IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
+        if (m_to_simplify.size() == 0)
+            return;
+        m_config.m_eqs_threshold = static_cast<unsigned>(10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size());
         m_config.m_expr_size_limit = 0;
         m_config.m_expr_degree_limit = 0;
         for (equation* e: m_to_simplify) {
@@ -87,9 +89,9 @@ namespace dd {
                    verbose_stream() << "set m_config.m_expr_degree_limit to " <<  m_config.m_expr_degree_limit << "\n";
                    );
         m_config.m_max_steps = 700;
-        m_config.m_max_simplified = 7000;        
+        m_config.m_max_simplified = 7000;
+        
     }
-
     void solver::saturate() {
         simplify();
         init_saturate();
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index 82c8a1c87..2308e5e46 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -55,7 +55,6 @@ public:
         unsigned m_max_simplified;
         unsigned m_random_seed;
         bool     m_enable_exlin;
-        unsigned m_eqs_growth;
         config() :
             m_eqs_threshold(UINT_MAX),
             m_expr_size_limit(UINT_MAX),
@@ -154,7 +153,7 @@ private:
     bool try_simplify_using(equation& target, equation const& source, bool& changed_leading_term);
 
     bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }    
-    bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
+    bool is_simpler(equation const& eq1, equation const& eq2) { return m.lm_lt(eq1.poly(), eq2.poly()); }
     bool is_conflict(equation const* eq) const { return is_conflict(*eq); }
     bool is_conflict(equation const& eq) const { return eq.poly().is_val() && !is_trivial(eq); }
     bool check_conflict(equation& eq) { return is_conflict(eq) && (set_conflict(eq), true); }    
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index ecf810894..0995fa7d2 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -143,90 +143,179 @@ void test_iterator() {
 class test {
 public :
     static void order() {
-    std::cout << "order\n";
-    pdd_manager m(4);
-    unsigned va = 0;
-    unsigned vb = 1;
-    unsigned vc = 2;
-    unsigned vd = 3;
-    pdd a = m.mk_var(va);
-    pdd b = m.mk_var(vb);
-    pdd c = m.mk_var(vc);
-    pdd d = m.mk_var(vd);
-    pdd p = a + b;
-    std::cout << p << "\n";
-    unsigned i = 0;
-    for (auto const& m : p) {
-        std::cout << m << "\n";        
-        SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
-        SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
-        i++;
-    }
-    pdd ccbbaa = c*c*b*b*a*a;
-    pdd ccbbba = c*c*b*b*b*a;
-    p = ccbbaa + ccbbba;
+        std::cout << "order\n";
+        pdd_manager m(4);
+        unsigned va = 0;
+        unsigned vb = 1;
+        unsigned vc = 2;
+        unsigned vd = 3;
+        pdd a = m.mk_var(va);
+        pdd b = m.mk_var(vb);
+        pdd c = m.mk_var(vc);
+        pdd d = m.mk_var(vd);
+        pdd p = a + b;
+        std::cout << p << "\n";
+        unsigned i = 0;
+        for (auto const& m : p) {
+            std::cout << m << "\n";        
+            SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
+            SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
+            i++;
+        }
+        pdd ccbbaa = c*c*b*b*a*a;
+        pdd ccbbba = c*c*b*b*b*a;
+        p = ccbbaa + ccbbba;
 
-    i = 0;
-    std::cout << "p = " <<  p << "\n";
-    for (auto const& m : p) {
-        std::cout << m << "\n";
-        SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
-        SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
-        i++;
-    }
-    pdd dcbba = d*c*b*b*a;
-    pdd dd = d * d;
-    p = dcbba + ccbbba + dd;
-    vector<unsigned> v;
-    std::cout << "p = " <<  p << "\n";
-    unsigned k = p.index();
-    std::cout << "pdd(k) = " << pdd(k, m) << "\n";
-    k = m.first_leading(k);
-    do {
-        if (m.is_val(k)) {
-            SASSERT(m.val(k).is_one());
-            break;
+        i = 0;
+        std::cout << "p = " <<  p << "\n";
+        for (auto const& m : p) {
+            std::cout << m << "\n";
+            SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
+            SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
+            i++;
         }
-        v.push_back(m.var(k));        
+        pdd dcbba = d*c*b*b*a;
+        pdd dd = d * d;
+        p = dcbba + ccbbba + dd;
+        vector<unsigned> v;
+        std::cout << "p = " <<  p << "\n";
+        unsigned k = p.index();
         std::cout << "pdd(k) = " << pdd(k, m) << "\n";
-        std::cout << "push v" << m.var(k) << "\n";
-        k = m.next_leading(k);
-    } while(true);
-    auto it = v.begin();
-    std::cout << "v" << *it;
-    it++;
-    for( ; it != v.end(); it ++) {
-        std::cout << "*v" << *it;
-    }
-    SASSERT(v.size() == 6);
-    SASSERT(v[0] == vc);
-    std::cout << "\n";
-    v.reset();
-    p = d*c*c*d + b*c*c*b + d*d*d;
-    k = p.index();
-    std::cout << "pdd(k) = " << pdd(k, m) << "\n";
-    k = m.first_leading(k);
-    do {
-        if (m.is_val(k)) {
-            SASSERT(m.val(k).is_one());
-            break;
+        k = m.first_leading(k);
+        do {
+            if (m.is_val(k)) {
+                SASSERT(m.val(k).is_one());
+                break;
+            }
+            v.push_back(m.var(k));        
+            std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+            std::cout << "push v" << m.var(k) << "\n";
+            k = m.next_leading(k);
+        } while(true);
+        auto it = v.begin();
+        std::cout << "v" << *it;
+        it++;
+        for( ; it != v.end(); it ++) {
+            std::cout << "*v" << *it;
         }
-        v.push_back(m.var(k));        
+        SASSERT(v.size() == 6);
+        SASSERT(v[0] == vc);
+        std::cout << "\n";
+        v.reset();
+        p = d*c*c*d + b*c*c*b + d*d*d;
+        k = p.index();
         std::cout << "pdd(k) = " << pdd(k, m) << "\n";
-        std::cout << "push v" << m.var(k) << "\n";
-        k = m.next_leading(k);
-    } while(true);
-    it = v.begin();
-    std::cout << "v" << *it;
-    it++;
-    for( ; it != v.end(); it ++) {
-        std::cout << "*v" << *it;
-    }
-    SASSERT(v.size() == 4);
-    SASSERT(v[0] == vd);
-    std::cout << "\n";
+        k = m.first_leading(k);
+        do {
+            if (m.is_val(k)) {
+                SASSERT(m.val(k).is_one());
+                break;
+            }
+            v.push_back(m.var(k));        
+            std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+            std::cout << "push v" << m.var(k) << "\n";
+            k = m.next_leading(k);
+        } while(true);
+        it = v.begin();
+        std::cout << "v" << *it;
+        it++;
+        for( ; it != v.end(); it ++) {
+            std::cout << "*v" << *it;
+        }
+        SASSERT(v.size() == 4);
+        SASSERT(v[0] == vd);
+        std::cout << "\n";
     
-}
+    }
+    static void order_lm() {
+        std::cout << "order_lm\n";
+        pdd_manager m(4);
+        unsigned va = 0;
+        unsigned vb = 1;
+        unsigned vc = 2;
+        unsigned vd = 3;
+        pdd a = m.mk_var(va);
+        pdd b = m.mk_var(vb);
+        pdd c = m.mk_var(vc);
+        pdd d = m.mk_var(vd);
+        pdd p = a + b;
+        std::cout << p << "\n";
+        unsigned i = 0;
+        for (auto const& m : p) {
+            std::cout << m << "\n";        
+            SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
+            SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
+            i++;
+        }
+        pdd ccbbaa = c*c*b*b*a*a;
+        pdd ccbbba = c*c*b*b*b*a;
+        p = ccbbaa + ccbbba;
+
+        i = 0;
+        std::cout << "p = " <<  p << "\n";
+        for (auto const& m : p) {
+            std::cout << m << "\n";
+            SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
+            SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
+            i++;
+        }
+        pdd dcbba = d*c*b*b*a;
+        pdd dd = d * d;
+        pdd p0 = p + dd;
+        std::cout << p0 << " > " << p << "\n";
+        SASSERT(m.lm_lt(p, p0));
+        SASSERT(m.lm_lt(p0 + a * b, p0 + b * b));
+        
+        // vector<unsigned> v;
+        // std::cout << "p = " <<  p << "\n";
+        // unsigned k = p.index();
+        // std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+        // k = m.first_leading(k);
+        // do {
+        //     if (m.is_val(k)) {
+        //         SASSERT(m.val(k).is_one());
+        //         break;
+        //     }
+        //     v.push_back(m.var(k));        
+        //     std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+        //     std::cout << "push v" << m.var(k) << "\n";
+        //     k = m.next_leading(k);
+        // } while(true);
+        // auto it = v.begin();
+        // std::cout << "v" << *it;
+        // it++;
+        // for( ; it != v.end(); it ++) {
+        //     std::cout << "*v" << *it;
+        // }
+        // SASSERT(v.size() == 6);
+        // SASSERT(v[0] == vc);
+        // std::cout << "\n";
+        // v.reset();
+        // p = d*c*c*d + b*c*c*b + d*d*d;
+        // k = p.index();
+        // std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+        // k = m.first_leading(k);
+        // do {
+        //     if (m.is_val(k)) {
+        //         SASSERT(m.val(k).is_one());
+        //         break;
+        //     }
+        //     v.push_back(m.var(k));        
+        //     std::cout << "pdd(k) = " << pdd(k, m) << "\n";
+        //     std::cout << "push v" << m.var(k) << "\n";
+        //     k = m.next_leading(k);
+        // } while(true);
+        // it = v.begin();
+        // std::cout << "v" << *it;
+        // it++;
+        // for( ; it != v.end(); it ++) {
+        //     std::cout << "*v" << *it;
+        // }
+        // SASSERT(v.size() == 4);
+        // SASSERT(v[0] == vd);
+        // std::cout << "\n";
+    
+    }
 };
 
 }
@@ -239,4 +328,5 @@ void tst_pdd() {
     dd::test_reset();
     dd::test_iterator();
     dd::test::order();
+    dd::test::order_lm();
 }