mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

reset out_bits when blasting multiplication of bit-vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-05 10:16:02 -08:00
parent 9dfcaaa01d
commit fafdbfaf0e
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -159,6 +159,7 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
SASSERT(sz > 0); SASSERT(sz > 0);
numeral n_a, n_b; numeral n_a, n_b;
out_bits.reset();
if (is_numeral(sz, a_bits, n_b)) if (is_numeral(sz, a_bits, n_b))
std::swap(a_bits, b_bits); std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) { if (is_minus_one(sz, b_bits)) {