diff --git a/src/sat/smt/polysat_constraints.h b/src/sat/smt/polysat_constraints.h
index 24c7f9a11..156776517 100644
--- a/src/sat/smt/polysat_constraints.h
+++ b/src/sat/smt/polysat_constraints.h
@@ -39,6 +39,16 @@ namespace polysat {
         pdd m_lhs, m_rhs;
     public:
         ule_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
+        pdd const& lhs() const { return m_lhs; }
+        pdd const& rhs() const { return m_rhs; }
+    };
+
+    class umul_ovfl_constraint : public constraint {
+        pdd m_lhs, m_rhs;
+    public:
+        umul_ovfl_constraint(pdd const& lhs, pdd const& rhs) : m_lhs(lhs), m_rhs(rhs) {}
+        pdd const& lhs() const { return m_lhs; }
+        pdd const& rhs() const { return m_rhs; }
     };
 
     class signed_constraint {
@@ -54,8 +64,12 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_constraint->vars(); }
         unsigned var(unsigned idx) const { return m_constraint->var(idx); }
         bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
+        ckind_t op() const { return m_op; }
         bool is_ule() const { return m_op == ule_t; }
-        ule_constraint& to_ule() { return *reinterpret_cast<ule_constraint*>(m_constraint); }
+        bool is_umul_ovfl() const { return m_op == umul_ovfl_t; }
+        bool is_smul_fl() const { return m_op == smul_fl_t; }
+        ule_constraint const& to_ule() const { return *reinterpret_cast<ule_constraint*>(m_constraint); }
+        umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
         bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
     };
 
diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h
index 0c173da77..b3e7dead5 100644
--- a/src/sat/smt/polysat_core.h
+++ b/src/sat/smt/polysat_core.h
@@ -102,8 +102,6 @@ namespace polysat {
         bool propagate();
         void assign_eh(unsigned idx, signed_constraint const& sc, dependency const& dep);
 
-        expr_ref constraint2expr(signed_constraint const& sc) const { throw default_exception("nyi"); }
-
         pdd value(rational const& v, unsigned sz);
 
         signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 35b177754..84e06636e 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -113,7 +113,7 @@ namespace polysat {
         m_lemma_level = level;
         m_lemma.reset();
         for (auto sc : lemma)
-            m_lemma.push_back(m_core.constraint2expr(sc));
+            m_lemma.push_back(constraint2expr(sc));
         ctx.set_conflict(ex);
     }
 
@@ -172,7 +172,7 @@ namespace polysat {
     // The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
     // Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions. 
     void solver::propagate(signed_constraint sc, dependency_vector const& deps) {
-        sat::literal lit = ctx.mk_literal(m_core.constraint2expr(sc));
+        sat::literal lit = ctx.mk_literal(constraint2expr(sc));
         auto [core, eqs] = explain_deps(deps);
         auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
         ctx.propagate(lit, ex);
@@ -200,7 +200,7 @@ namespace polysat {
     void solver::add_lemma(vector<signed_constraint> const& lemma) {
         sat::literal_vector lits;
         for (auto sc : lemma)
-            lits.push_back(ctx.mk_literal(m_core.constraint2expr(sc)));
+            lits.push_back(ctx.mk_literal(constraint2expr(sc)));
         s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
     }
 
@@ -209,4 +209,35 @@ namespace polysat {
         ctx.get_th_antecedents(l, jst, r, probing);
     }
 
+    expr_ref solver::constraint2expr(signed_constraint const& sc) { 
+        switch (sc.op()) {
+        case ckind_t::ule_t: {
+            auto l = pdd2expr(sc.to_ule().lhs());
+            auto h = pdd2expr(sc.to_ule().rhs());
+            return expr_ref(bv.mk_ule(l, h), m);
+        }
+        case ckind_t::umul_ovfl_t: {
+            auto l = pdd2expr(sc.to_umul_ovfl().lhs());
+            auto r = pdd2expr(sc.to_umul_ovfl().rhs());
+            return expr_ref(bv.mk_bvumul_ovfl(l, r), m);
+        }
+        case ckind_t::smul_fl_t:
+        case ckind_t::op_t:
+            break;
+        }
+        throw default_exception("nyi"); 
+    }
+
+    expr_ref solver::pdd2expr(pdd const& p) {
+        if (p.is_val()) {
+            expr* n = bv.mk_numeral(p.val(), p.power_of_2());
+            return expr_ref(n, m);
+        }
+        auto lo = pdd2expr(p.lo());
+        auto hi = pdd2expr(p.hi());
+        auto v = var2enode(m_pddvar2var[p.var()]);
+        hi = bv.mk_bv_mul(v->get_expr(), hi);
+        return expr_ref(bv.mk_bv_add(lo, hi), m);
+    }
+
 }
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 7940a7223..6f8e7a640 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -139,6 +139,9 @@ namespace polysat {
         void add_lemma(vector<signed_constraint> const& lemma);
 
         std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
+
+        expr_ref constraint2expr(signed_constraint const& sc);
+        expr_ref pdd2expr(pdd const& p);
 	       
     public:
         solver(euf::solver& ctx, theory_id id);