diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp
index 7c3cb1344..b43ee6866 100644
--- a/src/sat/smt/polysat/constraints.cpp
+++ b/src/sat/smt/polysat/constraints.cpp
@@ -115,12 +115,23 @@ namespace polysat {
         return ult(p, rational::power_of_two(k));
     }
 
-    // 2^{N-i-1}* p >= 2^{N-1}
+    // 2^{N-i-1} p >= 2^{N-1}
     signed_constraint constraints::bit(pdd const& p, unsigned i) {
         unsigned N = p.manager().power_of_2();
         return uge(p * rational::power_of_two(N - i - 1), rational::power_of_two(N - 1));
     }
 
+    // 2^k p - 2^{k+lo} val < 2^{k+lo}
+    // where k = N - hi - 1
+    signed_constraint constraints::fixed(pdd const& p, unsigned hi, unsigned lo, rational const& val) {
+        unsigned const N = p.manager().power_of_2();
+        SASSERT(lo <= hi && hi < N);
+        unsigned const k = N - hi - 1;
+        rational const& ttk = rational::power_of_two(k);
+        rational const& ttkl = rational::power_of_two(k + lo);
+        return ult(ttk * p - ttkl * val, ttkl);
+    }
+
     bool signed_constraint::is_eq(pvar& v, rational& val) {
         if (m_sign)
             return false;
diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h
index e6bdbe183..bd7f93f74 100644
--- a/src/sat/smt/polysat/constraints.h
+++ b/src/sat/smt/polysat/constraints.h
@@ -184,6 +184,9 @@ namespace polysat {
         signed_constraint band(pdd const& a, pdd const& b, pdd const& r);
         signed_constraint bor(pdd const& a, pdd const& b, pdd const& r);
 
+        // p[hi:lo] = val, represented as inequality
+        signed_constraint fixed(pdd const& p, unsigned hi, unsigned lo, rational const& val);
+
         //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
         //signed_constraint odd(pdd const& p) { return ~even(p); }
     };