From bee742111a822151c3f47ef8b1c0fb1f19f2b189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 11:05:19 -0800 Subject: [PATCH] na --- src/api/c++/z3++.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 941f7cc0b..1d44467f1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -334,7 +334,7 @@ namespace z3 { func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); void recdef(func_decl, expr_vector const& args, expr const& body); - func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range); + func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range); expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); @@ -3425,13 +3425,13 @@ namespace z3 { Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); } - inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) { - array args(arity); - for (unsigned i = 0; i < arity; i++) { + inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) { + array args(domain.size()); + for (unsigned i = 0; i < domain.size(); i++) { check_context(domain[i], range); args[i] = domain[i]; } - Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range); + Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, args.size(), args.ptr(), range); check_error(); return func_decl(*this, f); } @@ -3943,7 +3943,7 @@ namespace z3 { static_cast(p)->m_final_eh(); } - static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) { + static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e, unsigned id) { user_propagator_base* p = static_cast(_p); scoped_cb _cb(p, cb); scoped_context ctx(p->ctx());