diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index a8ac93fde..ded6aa645 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -89,7 +89,7 @@ namespace opt {
     }
     void model_based_opt::def::dec_ref() {
         SASSERT(m_ref_count > 0);
-        ++m_ref_count;
+        --m_ref_count;
         if (m_ref_count == 0) 
             dealloc(this);            
     }
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index d44a24986..67d00240c 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -85,6 +85,7 @@ namespace opt {
         enum def_t { add_t, mul_t, div_t, const_t, var_t};
         struct def {
             def() = default;
+            virtual ~def() = default;
             static def* from_row(row const& r, unsigned x);           
             def_t m_type;
             unsigned m_ref_count = 0;
@@ -120,6 +121,12 @@ namespace opt {
                 if (d) d->inc_ref();
                 m_def = d;
             }
+            def_ref(def_ref const& other) : m_def(other.m_def) {
+                if (m_def) m_def->inc_ref();
+            }
+            def_ref(def_ref&& other) noexcept : m_def(other.m_def) {
+                other.m_def = nullptr;
+            }
             def_ref& operator=(def* d) {
                 if (d) d->inc_ref();
                 if (m_def) m_def->dec_ref();
@@ -136,6 +143,15 @@ namespace opt {
                 return *this;
             }
 
+            def_ref& operator=(def_ref&& d) noexcept {
+                if (&d == this)
+                    return *this;
+                if (m_def) m_def->dec_ref();
+                m_def = d.m_def;
+                d.m_def = nullptr;
+                return *this;
+            }
+
             def& operator*() { return *m_def; }
             def* operator->() { return m_def; }
             def const& operator*() const { return *m_def; }
@@ -146,15 +162,18 @@ namespace opt {
         struct add_def : public def {
             def* x, *y;
             add_def(def* x, def* y) : x(x), y(y) { m_type = add_t;  x->inc_ref(); y->inc_ref(); }
+            ~add_def() { x->dec_ref(); y->dec_ref(); }
         };
         struct mul_def : public def {
             def* x, *y;
             mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t;  x->inc_ref(); y->inc_ref(); }
+            ~mul_def() { x->dec_ref(); y->dec_ref(); }
         };
         struct div_def : public def {
             def* x;
             rational m_div{ 1 };
             div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); }
+            ~div_def() { x->dec_ref(); }
         };
         struct var_def : public def {
             var v;