From e0860ea17314324608de517ecb0aa07b115f3674 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 May 2021 13:31:31 -0700
Subject: [PATCH] fix #5279

---
 src/ast/datatype_decl_plugin.cpp | 1 -
 src/ast/datatype_decl_plugin.h   | 8 ++++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 152256c69..7190d5bf9 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -645,7 +645,6 @@ namespace datatype {
             return false;
         func_decl* c = get_accessor_constructor(f);
         SASSERT(n == 1);
-        std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n";
         if (is_constructor(args[0])) 
             return to_app(args[0])->get_decl() != c;
         return false;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 8b609073d..6ac438f16 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -103,10 +103,10 @@ namespace datatype {
 
     namespace param_size {
         class size {
-            unsigned m_ref;
+            unsigned m_ref{ 0 };
         public:
-            size(): m_ref(0) {}
-            virtual ~size() {}
+            size() {}
+            virtual ~size() { }
             void inc_ref() { ++m_ref; }
             void dec_ref();
             static size* mk_offset(sort_size const& s); 
@@ -197,7 +197,7 @@ namespace datatype {
         sort_ref_vector const& params() const { return m_params; }
         util& u() const { return m_util; }
         param_size::size* sort_size() { return m_sort_size; }
-        void set_sort_size(param_size::size* p) { m_sort_size = p; if (p) p->inc_ref(); m_sort = nullptr; }
+        void set_sort_size(param_size::size* p) { auto* q = m_sort_size;  m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; }
         def* translate(ast_translation& tr, util& u);
     };