From 5e95a226c57cd484c89bfc1d00d464ae490c024f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 24 Feb 2023 13:52:52 +0100
Subject: [PATCH] easy AND for size 1

---
 src/math/polysat/constraint_manager.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);
     }