From 89c91765f60055561ee6519834337cabcbc512a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Jan 2020 14:03:32 -0600 Subject: [PATCH] fix 2863 Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 2 ++ src/ast/datatype_decl_plugin.h | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 5ec895a07..bd0679c85 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -726,6 +726,8 @@ namespace datatype { param_size::size* sz; obj_map S; unsigned n = get_datatype_num_parameter_sorts(s); + if (!is_declared(s)) + return nullptr; def & d = get_def(s->get_name()); SASSERT(n == d.params().size()); for (unsigned i = 0; i < n; ++i) { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index ae6a1a9ce..aa139b4a9 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -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; p->inc_ref(); m_sort = nullptr; } + void set_sort_size(param_size::size* p) { m_sort_size = p; if (p) p->inc_ref(); m_sort = nullptr; } def* translate(ast_translation& tr, util& u); };