mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse!

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-11-24 18:10:54 +00:00
parent 4c5753f321
commit 213d816c0a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -229,7 +229,7 @@ struct bv_size_reduction_tactic::imp {
else {
// l < u
if (l.is_neg()) {
unsigned i_nb = (u - l).get_num_bits();
unsigned i_nb = (u - l).get_num_bits() + 1;
unsigned v_nb = m_util.get_bv_size(v);
if (i_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));