diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 41de7f6b2..2f62dc7b8 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3773,7 +3773,9 @@ namespace z3 { array _sorts(n); array _num_params(n); array _cons(n); - std::vector> _params_vec; + + // Use unique_ptr to manage array lifetimes since array is non-copyable + std::vector>> _params_vec; std::vector _params_ptrs; _params_vec.reserve(n); @@ -3782,8 +3784,8 @@ namespace z3 { for (unsigned i = 0; i < n; ++i) { _names[i] = names[i]; _num_params[i] = params[i].size(); - _params_vec.emplace_back(params[i]); - _params_ptrs.push_back(_params_vec[i].ptr()); + _params_vec.push_back(std::unique_ptr>(new array(params[i]))); + _params_ptrs.push_back(_params_vec[i]->ptr()); _cons[i] = *cons[i]; } Z3_mk_polymorphic_datatypes(*this, n, _names.ptr(), _num_params.ptr(), _params_ptrs.data(), _sorts.ptr(), _cons.ptr());