mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix saturation condition for bvor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-11 11:35:35 -08:00
parent 9fb86a4d4f
commit 4a2217a3e8
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/op_constraint.cpp
View file

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