mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 16:03:16 +00:00
Code Activity

use mk_ite utility instead of custom local function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-06-12 16:10:08 -07:00
parent a2ad90cba1
commit 93d5e3f28e
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1002,7 +1002,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
out.reset();
for (unsigned j = 0; j < sz; ++j) {
unsigned src = (Left ? (sz + j - p) : (j + p)) % sz;
mk_ite(bit_i, out_bits.get(src), out_bits.get(j), tmp));
mk_ite(bit_i, out_bits.get(src), out_bits.get(j), tmp);
out.push_back(tmp);
}
out_bits.reset();