diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index a34e442b4..a5475c75e 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -480,6 +480,8 @@ namespace polysat { return p; if (p.is_val() && q.is_val()) return p.manager().mk_val(bitwise_and(p.val(), q.val())); + if (p.power_of_2() == 1) + return p * q; return mk_op_term(op_constraint::code::and_op, p, q); }