mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Update z3++.h

Browse source 
simplify definition
This commit is contained in:
Nikolaj Bjorner 2021-12-19 11:53:01 -08:00
parent a7b1db611c
commit 6a039c2700
1 changed files with 3 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/api/c++/z3++.h
View file

@ -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);
}