mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +00:00
Code Activity

Fix C++ binding compilation error - use unique_ptr for non-copyable array class

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-01 01:40:03 +00:00
parent 77de07db5a
commit 18ece378ee
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3773,7 +3773,9 @@ namespace z3 {
array<Z3_sort> _sorts(n); array<Z3_sort> _sorts(n);
array<unsigned> _num_params(n); array<unsigned> _num_params(n);
array<Z3_constructor_list> _cons(n); array<Z3_constructor_list> _cons(n);
std::vector<array<Z3_sort>> _params_vec;
// Use unique_ptr to manage array lifetimes since array is non-copyable
std::vector<std::unique_ptr<array<Z3_sort>>> _params_vec;
std::vector<Z3_sort const*> _params_ptrs; std::vector<Z3_sort const*> _params_ptrs;
_params_vec.reserve(n); _params_vec.reserve(n);
@ -3782,8 +3784,8 @@ namespace z3 {
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
_names[i] = names[i]; _names[i] = names[i];
_num_params[i] = params[i].size(); _num_params[i] = params[i].size();
_params_vec.emplace_back(params[i]); _params_vec.push_back(std::unique_ptr<array<Z3_sort>>(new array<Z3_sort>(params[i])));
_params_ptrs.push_back(_params_vec[i].ptr()); _params_ptrs.push_back(_params_vec[i]->ptr());
_cons[i] = *cons[i]; _cons[i] = *cons[i];
} }
Z3_mk_polymorphic_datatypes(*this, n, _names.ptr(), _num_params.ptr(), _params_ptrs.data(), _sorts.ptr(), _cons.ptr()); Z3_mk_polymorphic_datatypes(*this, n, _names.ptr(), _num_params.ptr(), _params_ptrs.data(), _sorts.ptr(), _cons.ptr());