fix saturation condition for bvor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 11, 2024 · 4a2217a · 4a2217a
1 parent 9fb86a4
commit 4a2217a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp
@@ -506,9 +506,9 @@ namespace polysat {
             bool rb = rv.val().get_bit(i);
             if (rb == (pb || qb))
                 continue;
-            if (pb && !qb && rb)
+            if (pb && !rb)
                 add_conflict(c, "p[i] => (p|q)[i]", { ~C.bit(p, i), C.bit(r, i) });
-            else if (!pb && qb && rb)
+            else if (qb && !rb)
                 add_conflict(c, "q[i] => (p|q)[i]", { ~C.bit(q, i), C.bit(r, i) });
             else if (!pb && !qb && rb)
                 add_conflict(c, "(p|q)[i] => p[i] or q[i]", { C.bit(p, i), C.bit(q, i), ~C.bit(r, i) });