diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index cfc5d3e4f..9a1d7c7d2 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -375,6 +375,9 @@ namespace polysat {
         case code::lshr_op:
             us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep);
             break;
+        case code::shl_op:
+            us.add_shl(p_coeff, q_coeff, r_coeff, !is_positive, dep);
+            break;
         case code::and_op:
             us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep);
             break;