diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h
index d51bcd839..ee26fe639 100644
--- a/src/sat/smt/polysat/core.h
+++ b/src/sat/smt/polysat/core.h
@@ -183,6 +183,8 @@ namespace polysat {
         assignment& get_assignment() { return m_assignment; }
 
         random_gen& rand() { return m_rand; }
+
+        pdd mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) { return s.mk_ite(sc, p, q); }
     };
 
 }
diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp
index cf235dafd..faa5a7b93 100644
--- a/src/sat/smt/polysat/monomials.cpp
+++ b/src/sat/smt/polysat/monomials.cpp
@@ -118,6 +118,8 @@ namespace polysat {
 
     // bit blast a monomial definition
     lbool monomials::bit_blast() {
+        // disable for now
+        return l_undef;
         init_to_refine();
         if (m_to_refine.empty())
             return l_true;
@@ -330,7 +332,17 @@ namespace polysat {
     }
 
     bool monomials::bit_blast(monomial const& mon) {
-        return false;
+        if (mon.size() != 2)
+            return false;
+        unsigned sz = mon.num_bits();
+        pdd n = mon.var.manager().mk_val(0);
+        pdd zero = n.manager().mk_val(0);
+        pdd p = mon.args[0];
+        pdd q = mon.args[1];
+        for (unsigned i = 0; i < sz; ++i) 
+            n += c.mk_ite(C.bit(p, i), c.value(rational::power_of_two(i), sz) * q, zero);
+        c.add_axiom("bit-blast", { C.eq(mon.var, n) }, true);
+        return true;
     }
 
     std::ostream& monomials::display(std::ostream& out) const {
diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index 8fa891b66..af83b2839 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -147,6 +147,7 @@ namespace polysat {
         virtual void get_bitvector_sub_slices(pvar v, offset_slices& out) = 0;
         virtual void get_bitvector_super_slices(pvar v, offset_slices& out) = 0;
         virtual void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice) = 0;
+        virtual pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) = 0;
         virtual unsigned level(dependency const& d) = 0;
     };
 
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index de0469bea..617d6c161 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -720,6 +720,21 @@ namespace polysat {
         mk_atom(lit.var(), sc);
     }
 
+    pdd solver::mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) {
+        expr_ref cond = constraint2expr(sc);
+        expr_ref th = pdd2expr(p);
+        expr_ref el = pdd2expr(q);
+        expr* ite = m.mk_ite(cond, th, el);
+        ctx.internalize(ite);
+        euf::enode* n = expr2enode(ite);
+        if (!n->is_attached_to(get_id())) {
+            auto v = mk_var(n);
+            pvar r = m_core.add_var(bv.get_bv_size(th));
+            internalize_set(v, m_core.var(r));
+        }
+        return expr2pdd(ite);
+    }
+
     dd::pdd solver::expr2pdd(expr* e) {
         return var2pdd(get_th_var(e));
     }
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 50fe60bc9..4b6be64c0 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -215,6 +215,7 @@ namespace polysat {
         void get_bitvector_super_slices(pvar v, offset_slices& out) override;
         void get_bitvector_suffixes(pvar v, offset_slices& out) override;
         void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits) override;
+        pdd  mk_ite(signed_constraint const& sc, pdd const& p, pdd const& q) override;
         unsigned level(dependency const& d) override;
         dependency explain_slice(pvar v, pvar w, unsigned offset);