From c2603cc4499e55fbe7ffca85df350872db259344 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 7 Feb 2026 19:32:17 +0000 Subject: [PATCH 1/2] Initial plan From 8b42b190a025f12da4cf829b7bed02f6acdd137a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 7 Feb 2026 19:49:28 +0000 Subject: [PATCH 2/2] Fix build warnings: cast size_t to unsigned in arith_decl_plugin.h and bv_decl_plugin.h Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/arith_decl_plugin.h | 8 ++++---- src/ast/bv_decl_plugin.h | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index a57d7ce07..5172226ae 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -503,13 +503,13 @@ public: app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); } - app* mk_band(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, args.size(), args.begin()); } + app* mk_band(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, static_cast(args.size()), args.begin()); } app* mk_shl(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, 2, args); } - app* mk_shl(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, args.size(), args.begin()); } + app* mk_shl(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, static_cast(args.size()), args.begin()); } app* mk_ashr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, 2, args); } - app* mk_ashr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, args.size(), args.begin()); } + app* mk_ashr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, static_cast(args.size()), args.begin()); } app* mk_lshr(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, 2, args); } - app* mk_lshr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, args.size(), args.begin()); } + app* mk_lshr(unsigned n, std::initializer_list args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, static_cast(args.size()), args.begin()); } app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 3a4b50c9e..6bfc50898 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -500,17 +500,17 @@ public: return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n); } app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args); } - app * mk_concat(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_CONCAT, args.size(), args.begin()); } + app * mk_concat(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_CONCAT, static_cast(args.size()), args.begin()); } app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(expr_ref_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(ptr_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_concat(ptr_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data()); } app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args); } - app * mk_bv_or(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BOR, args.size(), args.begin()); } + app * mk_bv_or(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BOR, static_cast(args.size()), args.begin()); } app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args); } - app * mk_bv_and(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BAND, args.size(), args.begin()); } + app * mk_bv_and(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BAND, static_cast(args.size()), args.begin()); } app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args); } - app * mk_bv_xor(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BXOR, args.size(), args.begin()); } + app * mk_bv_xor(std::initializer_list args) { return m_manager.mk_app(get_fid(), OP_BXOR, static_cast(args.size()), args.begin()); } app * mk_concat(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_concat(2, args); } app * mk_bv_and(expr* x, expr* y) { expr* args[2] = { x, y }; return mk_bv_and(2, args); }