mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Add gcd test to bv-rewriter

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-20 11:09:44 -08:00
parent 6506d33b35
commit a475e7cf5a
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2616,6 +2616,11 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
} }
if (!gcd_test(lhs, rhs)) {
result = m().mk_false();
return BR_DONE;
}
br_status st; br_status st;
if (m_bit2bool) { if (m_bit2bool) {
st = mk_bit2bool(lhs, rhs, result); st = mk_bit2bool(lhs, rhs, result);