mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Update bit_blaster_tpl_def.h

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-16 09:34:25 -06:00 • committed by GitHub
parent 969828b701
commit eb775b2206
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -769,10 +769,9 @@ template<typename Cfg>
void bit_blaster_tpl<Cfg>::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);
out_bits.reset();
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);
}