diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 7ded9bc53..7a7f2521e 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1148,6 +1148,7 @@ namespace dd {
     unsigned pdd_manager::max_pow2_divisor(PDD p) {
         init_mark();
         unsigned min_j = UINT_MAX;
+        SASSERT(m_todo.empty());
         m_todo.push_back(p);
         while (!m_todo.empty()) {
             PDD r = m_todo.back();
@@ -1986,5 +1987,32 @@ namespace dd {
         return out;
     }
 
+    void pdd_linear_iterator::first() {
+        m_next = m_pdd.root;
+        next();
+    }
 
-}
+    void pdd_linear_iterator::next() {
+        SASSERT(m_next != pdd_manager::null_pdd);
+        auto& m = m_pdd.manager();
+        while (!m.is_val(m_next)) {
+            unsigned const var = m.var(m_next);
+            rational const val = m.offset(m.hi(m_next));
+            m_next = m.lo(m_next);
+            if (!val.is_zero()) {
+                m_mono = {val, var};
+                return;
+            }
+        }
+        m_next = pdd_manager::null_pdd;
+    }
+
+    pdd_linear_iterator pdd::pdd_linear_monomials::begin() const {
+        return pdd_linear_iterator(m_pdd, true);
+    }
+
+    pdd_linear_iterator pdd::pdd_linear_monomials::end() const {
+        return pdd_linear_iterator(m_pdd, false);
+    }
+
+}  // namespace dd
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index f63cf7bc7..35a7894a8 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -45,6 +45,7 @@ namespace dd {
     class pdd;
     class pdd_manager;
     class pdd_iterator;
+    class pdd_linear_iterator;
 
     class pdd_manager {
     public:
@@ -53,13 +54,14 @@ namespace dd {
         friend test;
         friend pdd;
         friend pdd_iterator;
+        friend pdd_linear_iterator;
 
         typedef unsigned PDD;
         typedef vector<std::pair<rational,unsigned_vector>> monomials_t;
 
-        const PDD null_pdd = UINT_MAX;
-        const PDD zero_pdd = 0;
-        const PDD one_pdd = 1;
+        static constexpr PDD null_pdd = UINT_MAX;
+        static constexpr PDD zero_pdd = 0;
+        static constexpr PDD one_pdd = 1;
 
         enum pdd_op {
             pdd_add_op = 2,
@@ -400,6 +402,7 @@ namespace dd {
         friend test;
         friend class pdd_manager;
         friend class pdd_iterator;
+        friend class pdd_linear_iterator;
         unsigned     root;
         pdd_manager* m;
         pdd(unsigned root, pdd_manager& pm): root(root), m(&pm) { m->inc_ref(root); }
@@ -501,6 +504,16 @@ namespace dd {
         pdd_iterator begin() const;
         pdd_iterator end() const;
 
+        class pdd_linear_monomials {
+            friend class pdd;
+            pdd const& m_pdd;
+            pdd_linear_monomials(pdd const& p): m_pdd(p) {}
+        public:
+            pdd_linear_iterator begin() const;
+            pdd_linear_iterator end() const;
+        };
+        pdd_linear_monomials linear_monomials() const { return pdd_linear_monomials(*this); }
+
         pdd_manager& manager() const { return *m; }
     };
 
@@ -558,6 +571,26 @@ namespace dd {
         bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
     };
 
+    class pdd_linear_iterator {
+        friend class pdd::pdd_linear_monomials;
+        pdd m_pdd;
+        std::pair<rational, unsigned> m_mono;
+        pdd_manager::PDD m_next = pdd_manager::null_pdd;
+        pdd_linear_iterator(pdd const& p, bool at_start): m_pdd(p) { if (at_start) first(); }
+        void first();
+        void next();
+    public:
+        using value_type = std::pair<rational, unsigned>;  // coefficient and variable
+        using reference = value_type const&;
+        using pointer = value_type const*;
+        reference operator*() const { return m_mono; }
+        pointer operator->() const { return &m_mono; }
+        pdd_linear_iterator& operator++() { next(); return *this; }
+        pdd_linear_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
+        bool operator==(pdd_linear_iterator const& other) const { return m_next == other.m_next; }
+        bool operator!=(pdd_linear_iterator const& other) const { return m_next != other.m_next; }
+    };
+
     class val_pp {
         pdd_manager const& m;
         rational const& val;