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

Fix bvnego (#6750)

Browse source
This commit is contained in:
Jakob Rath 2023-06-07 20:24:40 +02:00 • committed by GitHub
parent 73c3f34d66
commit 57e92b2a59
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3015,8 +3015,8 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args,
br_status bv_rewriter::mk_bvneg_overflow(expr * const arg, expr_ref & result) { br_status bv_rewriter::mk_bvneg_overflow(expr * const arg, expr_ref & result) {
unsigned int sz = get_bv_size(arg); unsigned int sz = get_bv_size(arg);
auto maxUnsigned = mk_numeral(rational::power_of_two(sz)-1, sz); auto minSigned = mk_numeral(rational::power_of_two(sz - 1), sz); // 0b1000...0
result = m.mk_eq(arg, maxUnsigned); result = m.mk_eq(arg, minSigned);
return BR_REWRITE3; return BR_REWRITE3;
} }
@ -3085,7 +3085,7 @@ br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, exp
SASSERT(num == 2); SASSERT(num == 2);
SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); SASSERT(get_bv_size(args[0]) == get_bv_size(args[1]));
auto sz = get_bv_size(args[0]); auto sz = get_bv_size(args[0]);
auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz);
expr_ref bvsaddo {m}; expr_ref bvsaddo {m};
expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) }; expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) };
auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo); auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo);
@ -3098,7 +3098,7 @@ br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, exp
SASSERT(num == 2); SASSERT(num == 2);
SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); SASSERT(get_bv_size(args[0]) == get_bv_size(args[1]));
auto sz = get_bv_size(args[1]); auto sz = get_bv_size(args[1]);
auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz);
auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz); auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz);
result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne)); result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne));
return BR_REWRITE_FULL; return BR_REWRITE_FULL;