Update z3++.h

simplify definition
Z3Prover · Dec 19, 2021 · 6a039c2 · 6a039c2
1 parent a7b1db6
commit 6a039c2
Showing 1 changed file with 3 additions and 6 deletions.
diff --git 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<Z3_sort> 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<Z3_sort> 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);
     }