fix #5279

Z3Prover · May 19, 2021 · e0860ea · e0860ea
1 parent ec03467
commit e0860ea
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git 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
@@ -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);
     };