mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

fix 2863

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-18 14:03:32 -06:00
parent 495b88ce99
commit 89c91765f6
2 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.cpp
View file

@ -726,6 +726,8 @@ namespace datatype {
param_size::size* sz; param_size::size* sz;
obj_map<sort, param_size::size*> S; obj_map<sort, param_size::size*> S;
unsigned n = get_datatype_num_parameter_sorts(s); unsigned n = get_datatype_num_parameter_sorts(s);
if (!is_declared(s))
return nullptr;
def & d = get_def(s->get_name()); def & d = get_def(s->get_name());
SASSERT(n == d.params().size()); SASSERT(n == d.params().size());
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {

2
src/ast/datatype_decl_plugin.h
View file

@ -197,7 +197,7 @@ namespace datatype {
sort_ref_vector const& params() const { return m_params; } sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; } util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; } 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); def* translate(ast_translation& tr, util& u);
}; };