diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 6c7750b90..1168952d4 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -259,7 +259,6 @@ namespace dd {
         void reset(unsigned_vector const& level2var);
         void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
         unsigned_vector const& get_level2var() const { return m_level2var; }
-        unsigned_vector& get_level2var() { return m_level2var; }
 
         pdd mk_var(unsigned i);
         pdd mk_val(rational const& r);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 741558f35..cf96fe90f 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1596,17 +1596,20 @@ void core::set_active_vars_weights(nex_creator& nc) {
 
 void core::set_level2var_for_pdd_grobner() {
     unsigned n = m_pdd_manager.get_level2var().size();
-    unsigned_vector level2var(n);
+    unsigned_vector sorted_vars(n);
     for (unsigned j = 0; j < n; j++)
-        level2var[j] = j;
+        sorted_vars[j] = j;
     // sort that the larger weights are in beginning
-    std::sort(level2var.begin(), level2var.end(), [this](unsigned a, unsigned b) {
+    std::sort(sorted_vars.begin(), sorted_vars.end(), [this](unsigned a, unsigned b) {
                                                       unsigned wa = get_var_weight(a);
                                                       unsigned wb = get_var_weight(b);
-                                                      return wa > wb || (wa == wb && a > b); });
-    unsigned_vector& l2v = m_pdd_manager.get_level2var();
+                                                      return wa < wb || (wa == wb && a < b); });
+    
+    unsigned_vector l2v(n);
     for (unsigned j = 0; j < n; j++)
-        l2v[j] = level2var[j];
+        l2v[j] = sorted_vars[j];
+
+    m_pdd_manager.reset(l2v);
 }
 
 unsigned core::get_var_weight(lpvar j) const {
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index 9cf0f5d46..7152096bd 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -1,89 +1,71 @@
 #include "math/dd/dd_pdd.h"
-#include "math/dd/pdd_eval.h"
-#include "math/dd/pdd_interval.h"
 
 namespace dd {
-static void test1() {
-    pdd_manager m(3);
-    pdd v0 = m.mk_var(0);
-    pdd v1 = m.mk_var(1);
-    pdd v2 = m.mk_var(2);
-    std::cout << v0 << "\n";
-    std::cout << v1 << "\n";
-    std::cout << v2 << "\n";
-    pdd c1 = v0 * v1 * v2;
-    pdd c2 = v2 * v0 * v1;
-    std::cout << c1 << "\n";
-    SASSERT(c1 == c2);
+    static void test1() {
+        pdd_manager m(3);
+        pdd v0 = m.mk_var(0);
+        pdd v1 = m.mk_var(1);
+        pdd v2 = m.mk_var(2);
+        std::cout << v0 << "\n";
+        std::cout << v1 << "\n";
+        std::cout << v2 << "\n";
+        pdd c1 = v0 * v1 * v2;
+        pdd c2 = v2 * v0 * v1;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
 
-    c1 = v0 + v1 + v2;
-    c2 = v2 + v1 + v0;
-    std::cout << c1 << "\n";
-    SASSERT(c1 == c2);
+        c1 = v0 + v1 + v2;
+        c2 = v2 + v1 + v0;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
 
-    c1 = (v0+v1) * v2;
-    c2 = (v0*v2) + (v1*v2);
-    std::cout << c1 << "\n";
-    SASSERT(c1 == c2);
-    c1 = (c1 + 3) + 1;
-    c2 = (c2 + 1) + 3;
-    std::cout << c1 << "\n";
-    SASSERT(c1 == c2);
-    c1 = v0 - v1;
-    c2 = v1 - v0;
-    std::cout << c1 << " " << c2 << "\n";
+        c1 = (v0+v1) * v2;
+        c2 = (v0*v2) + (v1*v2);
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
+        c1 = (c1 + 3) + 1;
+        c2 = (c2 + 1) + 3;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
+        c1 = v0 - v1;
+        c2 = v1 - v0;
+        std::cout << c1 << " " << c2 << "\n";
 
-    c1 = v1*v2;
-    c2 = (v0*v2) + (v2*v2);
-    pdd c3 = m.zero();
-    VERIFY(m.try_spoly(c1, c2, c3));
-    std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
+        c1 = v1*v2;
+        c2 = (v0*v2) + (v2*v2);
+        pdd c3 = m.zero();
+        VERIFY(m.try_spoly(c1, c2, c3));
+        std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
 
-    c1 = v1*v2;
-    c2 = (v0*v2) + (v1*v1);
-    VERIFY(m.try_spoly(c1, c2, c3));
-    std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
+        c1 = v1*v2;
+        c2 = (v0*v2) + (v1*v1);
+        VERIFY(m.try_spoly(c1, c2, c3));
+        std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
 
-    c1 = (v0*v1) - (v0*v0);
-    c2 = (v0*v1*(v2 + v0)) + v2;
-    c3 = c2.reduce(c1);
-    std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
-}
-
-static void test2() {
-    std::cout << "\ntest2\n";
-    // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by  bc
-    pdd_manager m(4);
-    pdd a = m.mk_var(0);
-    pdd b = m.mk_var(1);
-    pdd c = m.mk_var(2);
-    pdd d = m.mk_var(3);
-    pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
-    std::cout << e << "\n";
-    pdd f = b * c;
-    pdd r_ef = m.reduce(e, f);
-    m.display(std::cout);
-    std::cout << "result of reduce " << e << " by " << f << " is " << r_ef <<  "\n";
-    pdd r_fe = m.reduce(f, e);
-    std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
-    VERIFY(r_fe == f);
-}
-
-static void test3() {
-    std::cout << "\ntest3\n";
-    pdd_manager m(4);
-    pdd a = m.mk_var(0);
-    pdd b = m.mk_var(1);
-    pdd c = m.mk_var(2);
-    pdd d = m.mk_var(3);
-        
-    pdd e = a + c;
-    for (unsigned i = 0; i < 5; i++) {
-        e = e * e;
+        c1 = (v0*v1) - (v0*v0);
+        c2 = (v0*v1*(v2 + v0)) + v2;
+        c3 = c2.reduce(c1);
+        std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
+    }
+
+    static void test2() {
+        std::cout << "\ntest2\n";
+        // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by  bc
+        pdd_manager m(4);
+        pdd a = m.mk_var(0);
+        pdd b = m.mk_var(1);
+        pdd c = m.mk_var(2);
+        pdd d = m.mk_var(3);
+        pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
+        std::cout << e << "\n";
+        pdd f = b * c;
+        pdd r_ef = m.reduce(e, f);
+        m.display(std::cout);
+        std::cout << "result of reduce " << e << " by " << f << " is " << r_ef <<  "\n";
+        pdd r_fe = m.reduce(f, e);
+        std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
+        VERIFY(r_fe == f);
     }
-    e = e * b;
-    //    std::cout << e << "\n";
-}
 
 static void test_reset() {
     std::cout << "\ntest reset\n";
@@ -128,19 +110,25 @@ static void test5() {
     SASSERT(e == f);        
 }
 
-static void test6() {
-    std::cout << "\ntest6\n";
-    pdd_manager m(5);
-    pdd a = m.mk_var(0);
-    pdd b = m.mk_var(1);
-    pdd c = m.mk_var(2);
-    pdd d = m.mk_var(3);
-    pdd e = a * b * b * d + 2*a*b*c + (b*c*d) + (b*c) + (c*d) + 3;
-    pdd f = a * d * c + a + d;
-    pdd l = m.zero();
-    VERIFY(m.try_spoly(e, f, l));
-    std::cout << "superpose\n" << e << "\nand\n" << f << "\nresult\n" << l << "\n"; 
-}
+    static void test_reset() {
+        std::cout << "\ntest reset\n";
+        pdd_manager m(4);
+        pdd a = m.mk_var(0);
+        pdd b = m.mk_var(1);
+        pdd c = m.mk_var(2);
+        pdd d = m.mk_var(3);
+        std::cout << (a + b)*(c + d) << "\n";
+
+        unsigned_vector l2v;
+        for (unsigned i = 0; i < 4; ++i) 
+            l2v.push_back(3 - i);
+        m.reset(l2v);
+        a = m.mk_var(0);
+        b = m.mk_var(1);
+        c = m.mk_var(2);
+        d = m.mk_var(3);
+        std::cout << (a + b)*(c + d) << "\n";
+    }
 
     void test_iterator() {
         std::cout << "test iterator\n";