From 6a039c2700e8e5ca04a913835fc3ab560cab0e84 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 11:53:01 -0800 Subject: [PATCH] Update z3++.h simplify definition --- src/api/c++/z3++.h | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1d44467f1..e323184bf 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3426,12 +3426,9 @@ namespace z3 { } 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_solver_propagate_declare(range.ctx(), name, args.size(), args.ptr(), range); + check_context(domain, range); + array domain1(domain); + Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range); check_error(); return func_decl(*this, f); }