diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 1cb17900f..37531d936 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -430,6 +430,9 @@ public: } app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args); } 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_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args); } app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args); }