From 4625454a385f50811d0f6db4347e6d6d23ffec67 Mon Sep 17 00:00:00 2001
From: Zachary Wimer <zwimer@users.noreply.github.com>
Date: Mon, 12 Apr 2021 13:37:05 -0700
Subject: [PATCH] Fix fixedpoint rc bug and fix optimize non-const bug (#5173)

* Fix fixedpoint rc bug and fix optimize non-const bug

* Fix indentation
---
 src/api/c++/z3++.h | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 198f429a1..1aa1e6eb7 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -275,7 +275,7 @@ namespace z3 {
         /**
            \brief Return a floating point sort.
            \c ebits is a number of exponent bits,
-           \c sbits	is a number of significand bits,
+           \c sbits is a number of significand bits,
            \pre where ebits must be larger than 1 and sbits must be larger than 2.
          */
         sort fpa_sort(unsigned ebits, unsigned sbits);
@@ -2836,9 +2836,8 @@ 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(o)  {
+        optimize(optimize const & o):object(o), m_opt(o.m_opt) {
             Z3_optimize_inc_ref(o.ctx(), o.m_opt);
-            m_opt = o.m_opt;
         }
         optimize(context& c, optimize& src):object(c) {
             m_opt = Z3_mk_optimize(c); 
@@ -2934,7 +2933,15 @@ namespace z3 {
         Z3_fixedpoint m_fp;
     public:
         fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
+        fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
         ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
+        fixedpoint & operator=(fixedpoint const & o) {
+            Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
+            Z3_fixedpoint_dec_ref(ctx(), m_fp);
+            m_fp = o.m_fp;
+            object::operator=(o);
+            return *this;
+        }
         operator Z3_fixedpoint() const { return m_fp; }
         void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
         void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }