mirror of
https://github.com/Z3Prover/z3
synced 2026-02-10 02:50:55 +00:00
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>
This commit is contained in:
parent
c2603cc449
commit
8b42b190a0
2 changed files with 8 additions and 8 deletions
|
|
@ -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<expr*> 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<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, static_cast<unsigned>(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<expr*> 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<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_SHL, 1, &p, static_cast<unsigned>(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<expr*> 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<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_ASHR, 1, &p, static_cast<unsigned>(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<expr*> 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<expr*> args) { parameter p(n); return m_manager.mk_app(arith_family_id, OP_ARITH_LSHR, 1, &p, static_cast<unsigned>(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); }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue