diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 1e19f5284..2c0af4e58 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -233,8 +233,8 @@ namespace polysat {
         return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true };
     }
 
-    signed_constraint constraint_manager::shr(pdd const& p, pdd const& q) {
-        return { dedup(alloc(shr_constraint, *this, p, q)), true };
+    signed_constraint constraint_manager::shr(pdd const& p, pdd const& q, pdd const& r) {
+        return { dedup(alloc(shr_constraint, *this, p, q, r)), true };
     }
 
 
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index b62e3b3f2..18efd270e 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -97,7 +97,7 @@ namespace polysat {
         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);
-        signed_constraint shr(pdd const& p, pdd const& q);
+        signed_constraint shr(pdd const& p, pdd const& q, pdd const& r);
 
         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/shr_constraint.cpp b/src/math/polysat/shr_constraint.cpp
index 81320dcb7..2f7a5b144 100644
--- a/src/math/polysat/shr_constraint.cpp
+++ b/src/math/polysat/shr_constraint.cpp
@@ -28,11 +28,13 @@ namespace polysat {
     }    
 
     lbool shr_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
-        if (p.is_val() && r.is_val()) {
-            if (p.val() >= p.manager().power_of_2())
+        if (q.is_val() && r.is_val()) {
+            auto& m = p.manager();
+            if (q.val() >= m.power_of_2())
                 return r.is_zero() ? l_true : l_false;            
-            if (r.is_val()) {
-                // todo
+            if (p.is_val()) {
+                pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned()));
+                return rr == r ? l_true : l_false;
             }
             // other cases when we know lower 
             // bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index cadd8aba9..6d59cf0cd 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -139,7 +139,7 @@ namespace polysat {
         auto& m = p.manager();
         unsigned sz = m.power_of_2();
         pdd r = m.mk_var(add_var(sz));
-        assign_eh(m_constraints.shr(r, p, q));
+        assign_eh(m_constraints.shr(p, q, r), null_dependency);
         return r;
     }