diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b81927474..4bb1acded 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2292,6 +2292,7 @@ namespace z3 { class optimize : public object { Z3_optimize m_opt; + public: class handle { unsigned m_h; @@ -2300,6 +2301,17 @@ namespace z3 { unsigned h() const { return m_h; } }; optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); } + optimize(optimize& o):object(c) { + Z3_optimize_inc_ref(o.ctx(), o.m_opt); + m_opt = o.m_opt; + } + optimize& operator=(optimize const& o) { + Z3_optimize_inc_rec(o.ctx(), o.m_opt); + Z3_optimize_dec_ref(ctx(), m_opt); + m_opt = o.m_opt; + m_ctx = o.m_ctx; + return *this; + } ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } operator Z3_optimize() const { return m_opt; } void add(expr const& e) {