From e08abb3213be4b1eabc4fcd3d519273f14de529c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 Aug 2019 10:06:33 +0800
Subject: [PATCH] fix #2504

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 11 +++++++----
 src/ast/datatype_decl_plugin.h   | 17 +++++++++--------
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 1089e0159..06af112c1 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -121,6 +121,7 @@ namespace datatype {
     };
 
     namespace param_size {
+        void  size::dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
         size* size::mk_offset(sort_size const& s) { return alloc(offset, s); }
         size* size::mk_param(sort_ref& p) { return alloc(sparam, p); }
         size* size::mk_plus(size* a1, size* a2) { return alloc(plus, a1, a2); }
@@ -545,7 +546,9 @@ namespace datatype {
 
         void plugin::remove(symbol const& s) {
             def* d = nullptr;
-            if (m_defs.find(s, d)) dealloc(d);
+            if (m_defs.find(s, d)) {
+                dealloc(d);
+            }
             m_defs.remove(s);
         }
 
@@ -722,14 +725,13 @@ namespace datatype {
         if (is_datatype(s)) {
             param_size::size* sz;
             obj_map<sort, param_size::size*> S;
-            sref_vector<param_size::size> refs;
             unsigned n = get_datatype_num_parameter_sorts(s);
             def & d = get_def(s->get_name());
             SASSERT(n == d.params().size());
             for (unsigned i = 0; i < n; ++i) {
                 sort* ps = get_datatype_parameter_sort(s, i);
                 sz = get_sort_size(params, ps);
-                refs.push_back(sz);
+                m_refs.push_back(sz);
                 S.insert(d.params().get(i), sz); 
             }            
             auto ss = d.sort_size();
@@ -737,7 +739,7 @@ namespace datatype {
                 d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite()));
                 ss = d.sort_size();
             }
-            return  ss->subst(S);
+            return ss->subst(S);
         }
         array_util autil(m);
         if (autil.is_array(s)) {
@@ -821,6 +823,7 @@ namespace datatype {
             }
             TRACE("datatype", tout << "set sort size " << s << "\n";);
             d.set_sort_size(param_size::size::mk_plus(s_add));
+            m_refs.reset();
         }
     }
     
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index c478daa7c..42a706904 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -108,7 +108,7 @@ namespace datatype {
             size(): m_ref(0) {}
             virtual ~size() {}
             void inc_ref() { ++m_ref; }
-            void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
+            void dec_ref();
             static size* mk_offset(sort_size const& s); 
             static size* mk_param(sort_ref& p); 
             static size* mk_plus(size* a1, size* a2); 
@@ -159,13 +159,13 @@ namespace datatype {
     };
 
     class def {
-        ast_manager&        m;
-        util&               m_util;
-        symbol              m_name;
-        unsigned            m_class_id;
-        param_size::size*   m_sort_size;
-        sort_ref_vector     m_params;
-        mutable sort_ref    m_sort;
+        ast_manager&            m;
+        util&                   m_util;
+        symbol                  m_name;
+        unsigned                m_class_id;
+        param_size::size*       m_sort_size;
+        sort_ref_vector         m_params;
+        mutable sort_ref        m_sort;
         ptr_vector<constructor> m_constructors;
     public:
         def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params):
@@ -304,6 +304,7 @@ namespace datatype {
         obj_map<sort, bool>                         m_is_enum;
         mutable obj_map<sort, bool>                 m_is_fully_interp;
         mutable ast_ref_vector                      m_asts;
+        sref_vector<param_size::size>               m_refs;
         ptr_vector<ptr_vector<func_decl> >          m_vectors;
         unsigned                                    m_start;
         mutable ptr_vector<sort>                    m_fully_interp_trail;