diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index d539489b2..8c760d7fb 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1825,6 +1825,14 @@ namespace dd {
         return *this;
     }
 
+    /* Reset pdd to 0. Allows re-assigning the pdd manager. */
+    void pdd::reset(pdd_manager& new_m) {
+        m->dec_ref(root);
+        root = 0;
+        m = &new_m;
+        SASSERT(is_zero());
+    }
+
     rational const& pdd::leading_coefficient() const {
         pdd p = *this;
         while (!p.is_val())
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index b01a95254..f63cf7bc7 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -413,6 +413,7 @@ namespace dd {
         pdd& operator=(rational const& k);
         // TODO: pdd& operator=(pdd&& other);  (just swap like move constructor?)
         ~pdd() { m->dec_ref(root); }
+        void reset(pdd_manager& new_m);
         pdd lo() const { return pdd(m->lo(root), m); }
         pdd hi() const { return pdd(m->hi(root), m); }
         unsigned index() const { return root; }