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 342ff5ed8..a4b5410f6 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -768,9 +768,10 @@ void bit_blaster_tpl::mk_smod(unsigned sz, expr * const * a_bits, expr * co template void bit_blaster_tpl::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) { expr_ref_vector out_bits(m()); + out_bits.reserve(sz); for (unsigned i = 0; i < sz; ++i) { mk_iff(a_bits[i], b_bits[i], out); - out_bits.push_back(out); + out_bits[i] = out; } mk_and(out_bits.size(), out_bits.data(), out); }