mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 02:46:16 +00:00
Code Activity

fix #6352

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-09-20 20:31:55 -07:00
parent 088898834c
commit 4518f4fe02
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/datatype_decl_plugin.cpp
View file

@ -904,18 +904,16 @@ namespace datatype {
bool util::is_well_founded(unsigned num_types, sort* const* sorts) { bool util::is_well_founded(unsigned num_types, sort* const* sorts) {
buffer<bool> well_founded(num_types, false); buffer<bool> well_founded(num_types, false);
obj_map<sort, unsigned> sort2id; obj_map<sort, unsigned> sort2id;
for (unsigned i = 0; i < num_types; ++i) { for (unsigned i = 0; i < num_types; ++i)
sort2id.insert(sorts[i], i); sort2id.insert(sorts[i], i);
}
unsigned num_well_founded = 0, id = 0; unsigned num_well_founded = 0, id = 0;
bool changed; bool changed;
ptr_vector<sort> subsorts; ptr_vector<sort> subsorts;
do { do {
changed = false; changed = false;
for (unsigned tid = 0; tid < num_types; tid++) { for (unsigned tid = 0; tid < num_types; tid++) {
if (well_founded[tid]) { if (well_founded[tid])
continue; continue;
}
sort* s = sorts[tid]; sort* s = sorts[tid];
def const& d = get_def(s); def const& d = get_def(s);
for (constructor const* c : d) { for (constructor const* c : d) {
@ -923,9 +921,12 @@ namespace datatype {
subsorts.reset(); subsorts.reset();
get_subsorts(a->range(), subsorts); get_subsorts(a->range(), subsorts);
for (sort* srt : subsorts) { for (sort* srt : subsorts) {
if (sort2id.find(srt, id) && !well_founded[id]) { if (sort2id.find(srt, id)) {
goto next_constructor; if (!well_founded[id])
goto next_constructor;
} }
else if (is_datatype(srt))
break;
} }
} }
changed = true; changed = true;