mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

Refactor mk_concat call sites to use std::initializer_list (#8494)

Browse source 
* Initial plan

* Refactor mk_concat call sites to use std::initializer_list

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-02-04 13:45:20 -08:00 • committed by Nikolaj Bjorner
parent 3b8825f619
commit 73f6dae095
6 changed files with 16 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_fpa.cpp
View file

@ -455,8 +455,7 @@ namespace smt {
SASSERT(to_app(bv_val_e)->get_num_args() == 3);
app_ref bv_val_a(m);
bv_val_a = to_app(bv_val_e.get());
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
cc_args = m_bv_util.mk_concat(3, args);
cc_args = m_bv_util.mk_concat({bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2)});
c = m.mk_eq(wrapped, cc_args);
assert_cnstr(c);
assert_cnstr(mk_side_conditions());