mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

easy AND for size 1

Browse source
This commit is contained in:
Jakob Rath 2023-02-24 13:52:52 +01:00
parent 133661d81b
commit 5e95a226c5
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/constraint_manager.cpp
View file

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