From 7febcd47ec65a1e165e28d15c564e70b030740de Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 30 Nov 2022 11:38:16 +0100 Subject: [PATCH] Forgot univariate shl --- src/math/polysat/op_constraint.cpp | 3 +++ 1 file changed, 3 insertions(+) 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;