From 8929c578c124ad0a835f74c22dc222d590cf7d20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Oct 2014 09:29:49 -0700 Subject: [PATCH] fix bug in mk_shl Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 285493690..a11d7fd1a 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -912,9 +912,9 @@ void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * con } else { out_bits.append(sz, a_bits); - expr_ref_vector new_out_bits(m()); for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector new_out_bits(m()); unsigned shift_i = 1 << i; for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); @@ -925,7 +925,7 @@ void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * con } out_bits.reset(); out_bits.append(new_out_bits); - if (shift_i > sz) break; + if (shift_i >= sz) break; } } }