diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 8c760d7fb..7ded9bc53 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1934,23 +1934,23 @@ namespace dd {
     std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
 
     void pdd_iterator::next() {
-        auto& m = m_pdd.m;
+        auto& m = m_pdd.manager();
         while (!m_nodes.empty()) {
             auto& p = m_nodes.back();
-            if (p.first && !m->is_val(p.second)) {
+            if (p.first && !m.is_val(p.second)) {
                 p.first = false;
                 m_mono.vars.pop_back();
-                unsigned n = m->lo(p.second);
-                if (m->is_val(n) && m->val(n).is_zero()) {
+                unsigned n = m.lo(p.second);
+                if (m.is_val(n) && m.val(n).is_zero()) {
                     m_nodes.pop_back();
                     continue;
                 }
-                while (!m->is_val(n)) {
+                while (!m.is_val(n)) {
                     m_nodes.push_back(std::make_pair(true, n));
-                    m_mono.vars.push_back(m->var(n));
-                    n = m->hi(n);
+                    m_mono.vars.push_back(m.var(n));
+                    n = m.hi(n);
                 }
-                m_mono.coeff = m->val(n);
+                m_mono.coeff = m.val(n);
                 break;
             }
             else {
@@ -1961,13 +1961,13 @@ namespace dd {
 
     void pdd_iterator::first() {
         unsigned n = m_pdd.root;
-        auto& m = m_pdd.m;
-        while (!m->is_val(n)) {
+        auto& m = m_pdd.manager();
+        while (!m.is_val(n)) {
             m_nodes.push_back(std::make_pair(true, n));
-            m_mono.vars.push_back(m->var(n));
-            n = m->hi(n);
+            m_mono.vars.push_back(m.var(n));
+            n = m.hi(n);
         }
-        m_mono.coeff = m->val(n);
+        m_mono.coeff = m.val(n);
     }
 
     pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }