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

fix #5802

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-30 10:42:34 -08:00
parent 2551631957
commit 913b90f7aa
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2828,7 +2828,10 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args,
if (sign1) a1_val = rational::power_of_two(bv_sz) - a1_val; if (sign1) a1_val = rational::power_of_two(bv_sz) - a1_val;
rational lim = rational::power_of_two(bv_sz-1); rational lim = rational::power_of_two(bv_sz-1);
rational r = a0_val * a1_val; rational r = a0_val * a1_val;
result = m().mk_bool_val((is_overflow == (sign0 != sign1)) || r < lim); if (is_overflow)
result = m().mk_bool_val(sign0 != sign1 || r < lim);
else
result = m().mk_bool_val(sign0 == sign1 || r <= lim);
return BR_DONE; return BR_DONE;
} }