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

fix bug in generation of non-recursive constructor, modular starting point shifts during recursive calls

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-05 11:31:50 -07:00
parent 394d54fa8b
commit a7ef33c136
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/datatype_decl_plugin.cpp
View file

@ -857,9 +857,9 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty); ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty);
// step 1) // step 1)
unsigned sz = constructors->size(); unsigned sz = constructors->size();
++m_start; unsigned start = ++m_start;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = (*constructors)[(j + m_start) % sz]; func_decl * c = (*constructors)[(j + start) % sz];
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
for (; i < num_args; i++) { for (; i < num_args; i++) {
@ -872,7 +872,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
} }
// step 2) // step 2)
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = (*constructors)[(j + m_start) % sz]; func_decl * c = (*constructors)[(j + start) % sz];
TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;