From e5b14ab6825f48fffd09c758066b6a0b7b930f2f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 May 2018 14:03:32 -0700
Subject: [PATCH] fix #1625

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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) {