diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index dfa28a64b..469ea7492 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -202,6 +202,17 @@ namespace polysat {
         return ~ule(b, a); 
     }
 
+    /**
+    * encode that the i'th bit of p is 1.
+    * It holds if p << (K - i - 1) >= 2^{K-1}, where K is the bit-width.
+    */
+    signed_constraint constraint_manager::bit(pdd const& p, unsigned i) {
+        unsigned K = p.manager().power_of_2();
+        pdd q = p * rational::power_of_two(K - i - 1);
+        rational msb = rational::power_of_two(K - 1);
+        return ule(p.manager().mk_val(msb), q);
+    }
+
     signed_constraint constraint_manager::mul_ovfl(pdd const& a, pdd const& b) {
         return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true };
     }
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 612eb5e94..2a963ec23 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -95,6 +95,7 @@ namespace polysat {
         signed_constraint sle(pdd const& a, pdd const& b);
         signed_constraint slt(pdd const& a, pdd const& b);
         signed_constraint mul_ovfl(pdd const& p, pdd const& q);
+        signed_constraint bit(pdd const& p, unsigned i);
 
         constraint *const* begin() const { return m_constraints.data(); }
         constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 1cc5c30f4..b5b9edde3 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -291,7 +291,7 @@ namespace polysat {
         signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
         signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); }
         signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_ovfl(q.manager().mk_val(p), q); }
-
+        signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
 
         /** Create and activate polynomial constraints. */
         void add_eq(pdd const& p, unsigned dep = null_dependency)                { assign_eh(eq(p), dep); }