diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 51e3813c0..f04e7324f 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -418,6 +418,7 @@ namespace dd {
         bool is_monomial() const { return m.is_monomial(root); }
         bool is_univariate() const { return m.is_univariate(root); }
         void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
+        vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
         bool is_never_zero() const { return m.is_never_zero(root); }
         bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
 
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index a8d65be05..b2dd72571 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -17,6 +17,7 @@ Author:
 #include "math/polysat/types.h"
 #include "math/polysat/interval.h"
 #include "math/polysat/search_state.h"
+#include "math/polysat/univariate/univariate_solver.h"
 
 namespace polysat {
 
@@ -213,9 +214,12 @@ namespace polysat {
         void unset_mark() { m_is_marked = false; }
         bool is_marked() const { return m_is_marked; }
 
-
         bool is_active() const { return m_is_active; }
         void set_active(bool f) { m_is_active = f; }
+
+        /// Assuming the constraint is univariate under the current assignment of 's',
+        /// adds the constraint to the univariate solver 'us'.
+        virtual void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0;
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
@@ -256,10 +260,11 @@ namespace polysat {
         void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
         inequality as_inequality() const { return get()->as_inequality(is_positive()); }
 
+        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); }
+
         sat::bool_var bvar() const { return m_constraint->bvar(); }
         sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
         constraint* get() const { return m_constraint; }
-        
 
         explicit operator bool() const { return !!m_constraint; }
         bool operator!() const { return !m_constraint; }
@@ -270,7 +275,6 @@ namespace polysat {
         bool is_eq() const;
         pdd const& eq() const;
 
-
         signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
 
         unsigned hash() const {
diff --git a/src/math/polysat/mul_ovfl_constraint.cpp b/src/math/polysat/mul_ovfl_constraint.cpp
index c52c999de..5ad4d3218 100644
--- a/src/math/polysat/mul_ovfl_constraint.cpp
+++ b/src/math/polysat/mul_ovfl_constraint.cpp
@@ -166,4 +166,10 @@ namespace polysat {
     bool mul_ovfl_constraint::operator==(constraint const& other) const {
         return other.is_mul_ovfl() && p() == other.to_mul_ovfl().p() && q() == other.to_mul_ovfl().q();
     }
+
+    void mul_ovfl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        us.add_umul_ovfl(p_coeff, q_coeff, !is_positive, dep);
+    }
 }
diff --git a/src/math/polysat/mul_ovfl_constraint.h b/src/math/polysat/mul_ovfl_constraint.h
index 22ea39273..e296c95c0 100644
--- a/src/math/polysat/mul_ovfl_constraint.h
+++ b/src/math/polysat/mul_ovfl_constraint.h
@@ -48,6 +48,8 @@ namespace polysat {
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
+
+        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 3c8b866d1..6046dffbc 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -298,4 +298,21 @@ namespace polysat {
 
         return l_undef;
     }
+
+    void op_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        auto r_coeff = s.subst(r()).get_univariate_coefficients();
+        switch (m_op) {
+        case code::lshr_op:
+            us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            break;
+        case code::and_op:
+            us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            break;
+        default:
+            NOT_IMPLEMENTED_YET();
+            break;
+        }
+    }
 }
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index e3dfec82d..05b112aeb 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -65,6 +65,8 @@ namespace polysat {
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
+
+        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }
diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp
index 446ff95fa..cd6e20aec 100644
--- a/src/math/polysat/smul_fl_constraint.cpp
+++ b/src/math/polysat/smul_fl_constraint.cpp
@@ -118,4 +118,13 @@ namespace polysat {
             && p() == other.to_smul_fl().p()
             && q() == other.to_smul_fl().q();
     }
+
+    void smul_fl_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+        auto p_coeff = s.subst(p()).get_univariate_coefficients();
+        auto q_coeff = s.subst(q()).get_univariate_coefficients();
+        if (is_overflow())
+            us.add_smul_ovfl(p_coeff, q_coeff, !is_positive, dep);
+        else
+            us.add_smul_udfl(p_coeff, q_coeff, !is_positive, dep);
+    }
 }
diff --git a/src/math/polysat/smul_fl_constraint.h b/src/math/polysat/smul_fl_constraint.h
index 7af9e91cc..1937b259c 100644
--- a/src/math/polysat/smul_fl_constraint.h
+++ b/src/math/polysat/smul_fl_constraint.h
@@ -45,6 +45,8 @@ namespace polysat {
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return false; }
+
+        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index de48ae9ba..cf041e2e9 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -207,4 +207,9 @@ namespace polysat {
         return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs();
     }
 
+    void ule_constraint::add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
+        auto p_coeff = s.subst(lhs()).get_univariate_coefficients();
+        auto q_coeff = s.subst(rhs()).get_univariate_coefficients();
+        us.add_ule(p_coeff, q_coeff, !is_positive, dep);
+    }
 }
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index 57fab0a1e..990c468a6 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -46,7 +46,7 @@ namespace polysat {
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return m_rhs.is_zero(); }
         bool is_diseq() const override { return m_lhs.is_one(); }
-        // pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
+        void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
 }