diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index f6ea3aadb..ecfd57eca 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -373,13 +373,14 @@ namespace polysat {
         }
 #endif
         constraint_dedup::quot_rem_args args({a, b});
-        auto it = m_dedup.quot_rem_expr.find_iterator(args);
-        if (it != m_dedup.quot_rem_expr.end())
+        auto it = m_dedup.m_quot_rem_expr.find_iterator(args);
+        if (it != m_dedup.m_quot_rem_expr.end())
             return { m.mk_var(it->m_value.first), m.mk_var(it->m_value.second) };
 
         pdd q = m.mk_var(s.add_var(sz));  // quotient
         pdd r = m.mk_var(s.add_var(sz));  // remainder
-        m_dedup.quot_rem_expr.insert(args, { q.var(), r.var() });
+        m_dedup.m_quot_rem_expr.insert(args, { q.var(), r.var() });
+        m_dedup.m_div_rem_list.push_back({ a, b, q.var(), r.var() });
 
         // Axioms for quotient/remainder:
         //      a = b*q + r
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 0cc9ba93b..8b4a5ba06 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -38,7 +38,8 @@ namespace polysat {
             }
         };
         using quot_rem_expr_map = map<quot_rem_args, std::pair<pvar, pvar>, quot_rem_args_hash, quot_rem_args_eq>;
-        quot_rem_expr_map quot_rem_expr;
+        quot_rem_expr_map m_quot_rem_expr;
+        vector<std::tuple<pdd, pdd, pvar, pvar>> m_div_rem_list;
     };
 
     // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
@@ -131,6 +132,9 @@ namespace polysat {
         constraint* const* begin() const { return m_constraints.data(); }
         constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
 
+        std::tuple<pdd, pdd, pvar, pvar> const* begin_div() const { return m_dedup.m_div_rem_list.data(); }
+        std::tuple<pdd, pdd, pvar, pvar> const* end_div() const { return m_dedup.m_div_rem_list.data() + m_dedup.m_div_rem_list.size(); }
+
         class clause_iterator {
             friend class constraint_manager;
             using storage_t = decltype(constraint_manager::m_clauses);