From 4a2217a3e8a49eb2f80041bbca4b2eb40a9aae3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jan 2024 11:35:35 -0800 Subject: [PATCH] fix saturation condition for bvor Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/op_constraint.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 73c85521d..9e997538a 100644 --- 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) });