diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f1053fc0c..d94b4f36b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -388,6 +388,7 @@ namespace z3 { template array(ast_vector_tpl const & v); ~array() { delete[] m_array; } + void resize(unsigned sz) { delete[] m_array; m_array = new T[sz]; } unsigned size() const { return m_size; } T & operator[](int i) { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } T const & operator[](int i) const { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } @@ -2239,8 +2240,8 @@ namespace z3 { check_error(); expr_vector result(ctx(), r); unsigned sz = result.size(); - levels = array(sz); - Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.c_ptr()); + levels.resize(sz); + Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr()); check_error(); return result; }