diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 32456445c..0c8aa520d 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1005,28 +1005,32 @@ namespace dd {
 
     unsigned pdd_manager::degree(PDD p, unsigned v) {
         init_mark();
-        unsigned level_v = level(v);
+        unsigned level_v = m_var2level[v];
         unsigned max_d = 0, d = 0;
         m_todo.push_back(p);
         while (!m_todo.empty()) {
             PDD r = m_todo.back();
-            if (is_marked(r)) 
+            if (is_marked(r))
                 m_todo.pop_back();
             else if (is_val(r))
                 m_todo.pop_back();
             else if (level(r) < level_v)
                 m_todo.pop_back();
             else if (level(r) == level_v) {
-                d = 1;
-                while (!is_val(hi(r)) && level(hi(r)) == level_v) {
+                d = 0;
+                do {
                     ++d;
+                    set_mark(r);
                     r = hi(r);
-                }
+                } while (!is_val(r) && level(r) == level_v);
                 max_d = std::max(d, max_d);
                 m_todo.pop_back();
             }
-            else 
-                m_todo.push_back(lo(r)).push_back(hi(r));                
+            else {
+                set_mark(r);
+                m_todo.pop_back();
+                m_todo.push_back(lo(r)).push_back(hi(r));
+            }
         }
         return max_d;
     }
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index a1f4765ea..8142cb311 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -322,6 +322,65 @@ public :
         SASSERT(!(2*a*b + 3*b + 2).is_never_zero());
     }
 
+    static void degree_of_variables() {
+        std::cout << "degree of variables\n";
+        pdd_manager m(4, pdd_manager::mod2N_e, 3);
+        unsigned va = 0;
+        unsigned vb = 1;
+        unsigned vc = 2;
+        pdd a = m.mk_var(va);
+        pdd b = m.mk_var(vb);
+        pdd c = m.mk_var(vc);
+
+        SASSERT(a.var() == va);
+        SASSERT(b.var() == vb);
+
+        SASSERT(a.degree(va) == 1);
+        SASSERT(a.degree(vb) == 0);
+        SASSERT(a.degree(vc) == 0);
+        SASSERT(c.degree(vc) == 1);
+        SASSERT(c.degree(vb) == 0);
+        SASSERT(c.degree(va) == 0);
+
+        {
+            pdd p = a * a * a;
+            SASSERT(p.degree(va) == 3);
+            SASSERT(p.degree(vb) == 0);
+        }
+
+        {
+            pdd p = b * a;
+            SASSERT(p.degree(va) == 1);
+            SASSERT(p.degree(vb) == 1);
+            SASSERT(p.degree(vc) == 0);
+        }
+
+        {
+            pdd p = (a*a*b + b*a*b + b + a*c)*a + b*b*c;
+            SASSERT(p.degree(va) == 3);
+            SASSERT(p.degree(vb) == 2);
+            SASSERT(p.degree(vc) == 1);
+        }
+
+        {
+            // check that skipping marked nodes works (1)
+            pdd p = b*a + c*a*a*a;
+            SASSERT(p.degree(va) == 3);
+        }
+
+        {
+            // check that skipping marked nodes works (2)
+            pdd p = (b+c)*(a*a*a);
+            SASSERT(p.degree(va) == 3);
+        }
+
+        {
+            // check that skipping marked nodes works (3)
+            pdd p = a*a*a*b*b*b*c + a*a*a*b*b*b;
+            SASSERT(p.degree(va) == 3);
+        }
+    }
+
 };
 
 }
@@ -336,4 +395,5 @@ void tst_pdd() {
     dd::test::order();
     dd::test::order_lm();
     dd::test::mod4_operations();
+    dd::test::degree_of_variables();
 }