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

fix(datatypes): update following @nikolajbjorner 's review

Browse source
This commit is contained in:
Simon Cruanes 2018-04-04 10:41:40 -05:00
parent 433f487ff2
commit d973b08247
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_datatype.cpp
View file

@ -412,7 +412,7 @@ namespace smt {
}
// explain the cycle root -> … -> app -> root
void theory_datatype::occurs_check_explain(enode * app, enode * const root) {
void theory_datatype::occurs_check_explain(enode * app, enode * root) {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
@ -424,8 +424,7 @@ namespace smt {
SASSERT(d->m_constructor);
if (app != d->m_constructor)
m_used_eqs.push_back(enode_pair(app, d->m_constructor));
bool found = m_parent.find(app->get_root(), app_parent);
SASSERT(found);
app_parent = m_parent[app->get_root()];
app = app_parent;
}

4
src/smt/theory_datatype.h
View file

@ -104,8 +104,8 @@ namespace smt {
theory_datatype * th;
public:
final_check_st(theory_datatype * th) : th(th) {
th->m_to_unmark.reset();
th->m_to_unmark2.reset();
SASSERT(th->m_to_unmark.empty());
SASSERT(th->m_to_unmark2.empty());
th->m_used_eqs.reset();
th->m_stack.reset();
th->m_parent.reset();