mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix(datatype): always use root nodes for the parent table

Browse source
This commit is contained in:
Simon Cruanes 2018-04-03 18:30:09 -05:00
parent e535cad480
commit 433f487ff2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_datatype.cpp
View file

@ -424,7 +424,7 @@ namespace smt {
SASSERT(d->m_constructor); SASSERT(d->m_constructor);
if (app != d->m_constructor) if (app != d->m_constructor)
m_used_eqs.push_back(enode_pair(app, d->m_constructor)); m_used_eqs.push_back(enode_pair(app, d->m_constructor));
bool found = m_parent.find(app, app_parent); bool found = m_parent.find(app->get_root(), app_parent);
SASSERT(found); SASSERT(found);
app = app_parent; app = app_parent;
} }
@ -455,7 +455,7 @@ namespace smt {
} }
// explore `arg` (with parent `app`) // explore `arg` (with parent `app`)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg, app); m_parent.insert(arg->get_root(), app);
oc_push_stack(arg); oc_push_stack(arg);
} }
} }