diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 0dbf3c6f9..857665583 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1291,6 +1291,27 @@ namespace dd {
         return *this; 
     }
 
+
+    /**
+     * \brief substitute variable v by r.
+     * This base line implementation is simplistic and does not use operator caching.
+     */
+    pdd pdd::subst_pdd(unsigned v, pdd const& r) const {
+        if (is_val())
+            return *this;
+        if (m.m_var2level[var()] < m.m_var2level[v])
+            return *this;
+        pdd l = lo().subst_pdd(v, r);
+        pdd h = hi().subst_pdd(v, r);
+        if (var() == v) 
+            return r*h + l;
+        else if (l == lo() && h == hi())
+            return *this;
+        else
+            return m.mk_var(v)*h + l;
+    }
+
+
     std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
 
     void pdd_iterator::next() {
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 78c447494..13c6c0605 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -367,6 +367,12 @@ namespace dd {
         pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
 
+        
+        /**
+         * \brief substitute variable v by r.
+         */
+        pdd subst_pdd(unsigned v, pdd const& r) const;
+
         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; }