mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix bug in mk_shl

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-02 09:29:49 -07:00
parent 928fc550a5
commit 8929c578c1
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -912,9 +912,9 @@ void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * con
} }
else { else {
out_bits.append(sz, a_bits); out_bits.append(sz, a_bits);
expr_ref_vector new_out_bits(m());
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector new_out_bits(m());
unsigned shift_i = 1 << i; unsigned shift_i = 1 << i;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m()); expr_ref new_out(m());
@ -925,7 +925,7 @@ void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * con
} }
out_bits.reset(); out_bits.reset();
out_bits.append(new_out_bits); out_bits.append(new_out_bits);
if (shift_i > sz) break; if (shift_i >= sz) break;
} }
} }
} }