diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8440104e8..288bcab4e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -4367,8 +4367,7 @@ app_ref fpa2bv_converter_wrapped::wrap(expr* e) { app_ref res(m); if (m_util.is_fp(e)) { - expr* cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; - expr_ref tmp(m_bv_util.mk_concat(3, cargs), m); + expr_ref tmp(m_bv_util.mk_concat({to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2)}), m); m_rw(tmp); res = to_app(tmp); } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 1db2534cb..6f6a121e4 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -924,9 +924,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { SASSERT(r2 < numeral(bv_size)); // (bvshl x k) -> (concat (extract [n-1-k:0] x) bv0:k) unsigned k = r2.get_unsigned(); - expr * new_args[2] = { m_mk_extract(bv_size - k - 1, 0, arg1), - mk_zero(k) }; - result = m_util.mk_concat(2, new_args); + result = m_util.mk_concat({m_mk_extract(bv_size - k - 1, 0, arg1), mk_zero(k)}); return BR_REWRITE2; } @@ -983,9 +981,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) { // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) SASSERT(r2.is_unsigned()); unsigned k = r2.get_unsigned(); - expr * new_args[2] = { mk_zero(k), - m_mk_extract(bv_size - 1, k, arg1) }; - result = m_util.mk_concat(2, new_args); + result = m_util.mk_concat({mk_zero(k), m_mk_extract(bv_size - 1, k, arg1)}); return BR_REWRITE2; } @@ -1327,11 +1323,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e unsigned shift; if (r2.is_power_of_two(shift)) { - expr * args[2] = { - mk_zero(bv_size - shift), - m_mk_extract(shift-1, 0, arg1) - }; - result = m_util.mk_concat(2, args); + result = m_util.mk_concat({mk_zero(bv_size - shift), m_mk_extract(shift-1, 0, arg1)}); return BR_REWRITE2; } @@ -1714,8 +1706,7 @@ br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) return BR_DONE; } else { - expr * args[2] = { mk_zero(n), arg }; - result = m_util.mk_concat(2, args); + result = m_util.mk_concat({mk_zero(n), arg}); return BR_REWRITE1; } } @@ -2245,8 +2236,7 @@ br_status bv_rewriter::mk_bv_rotate_left(unsigned n, expr * arg, expr_ref & resu result = arg; return BR_DONE; } - expr * args[2] = { m_mk_extract(sz - n - 1, 0, arg), m_mk_extract(sz - 1, sz - n, arg) }; - result = m_util.mk_concat(2, args); + result = m_util.mk_concat({m_mk_extract(sz - n - 1, 0, arg), m_mk_extract(sz - 1, sz - n, arg)}); return BR_REWRITE2; } @@ -2496,11 +2486,7 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re unsigned shift; if (is_numeral(x, v, bv_size) && v.is_power_of_two(shift)) { SASSERT(shift >= 1); - expr * args[2] = { - m_mk_extract(bv_size-shift-1, 0, y), - mk_zero(shift) - }; - result = m_util.mk_concat(2, args); + result = m_util.mk_concat({m_mk_extract(bv_size-shift-1, 0, y), mk_zero(shift)}); return BR_REWRITE2; } } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 474d1c958..c2c888885 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -775,11 +775,10 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu if (m_fm.is_nan(v)) { if (m_hi_fp_unspecified) { - expr * args[4] = { bu.mk_numeral(0, 1), - bu.mk_numeral(rational::minus_one(), x.get_ebits()), - bu.mk_numeral(0, x.get_sbits() - 2), - bu.mk_numeral(1, 1) }; - result = bu.mk_concat(4, args); + result = bu.mk_concat({bu.mk_numeral(0, 1), + bu.mk_numeral(rational::minus_one(), x.get_ebits()), + bu.mk_numeral(0, x.get_sbits() - 2), + bu.mk_numeral(1, 1)}); return BR_REWRITE1; } } diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp index 6770e335b..092d2561d 100644 --- a/src/qe/mbp/mbp_solve_plugin.cpp +++ b/src/qe/mbp/mbp_solve_plugin.cpp @@ -418,16 +418,13 @@ namespace mbp { lhs = e; unsigned sz = m_bv.get_bv_size(e); if (lo > 0 && hi + 1 < sz) { - expr* args[3] = { m_bv.mk_extract(sz-1, hi + 1, e), rhs, m_bv.mk_extract(lo - 1, 0, e)}; - rhs = m_bv.mk_concat(3, args); + rhs = m_bv.mk_concat({m_bv.mk_extract(sz-1, hi + 1, e), rhs, m_bv.mk_extract(lo - 1, 0, e)}); } else if (lo == 0 && hi + 1 < sz) { - expr* args[2] = { m_bv.mk_extract(sz-1, hi + 1, e), rhs }; - rhs = m_bv.mk_concat(2, args); + rhs = m_bv.mk_concat({m_bv.mk_extract(sz-1, hi + 1, e), rhs}); } else if (lo > 0 && hi + 1 == sz) { - expr* args[2] = { rhs, m_bv.mk_extract(lo - 1, 0, e) }; - rhs = m_bv.mk_concat(2, args); + rhs = m_bv.mk_concat({rhs, m_bv.mk_extract(lo - 1, 0, e)}); } else { return false; diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 8754745e6..7f39cd5ed 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -231,8 +231,7 @@ namespace fpa { else if (m_fpa_util.is_numeral(n, val)) { expr_ref bv_val_e(convert(n), m); VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c)); - expr* args[] = { a, b, c }; - expr_ref cc_args(m_bv_util.mk_concat(3, args), m); + expr_ref cc_args(m_bv_util.mk_concat({a, b, c}), m); // Require // wrap(n) = bvK // fp(extract(wrap(n)) = n diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 3b768b3f6..5afc26c97 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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());