mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
chore(datatype): small fixes
This commit is contained in:
parent
bf6928fec0
commit
8fd2d8a636
|
@ -452,7 +452,7 @@ namespace smt {
|
|||
|
||||
SASSERT(app->get_root() == root->get_root());
|
||||
if (app != root)
|
||||
m_used_eqs.push_back(enode_pair(app, root));
|
||||
m_used_eqs.push_back(enode_pair(app, root));
|
||||
}
|
||||
|
||||
// start exploring subgraph below `app`
|
||||
|
@ -511,7 +511,7 @@ namespace smt {
|
|||
|
||||
switch (op) {
|
||||
case ENTER:
|
||||
res = occurs_check_enter(app) || res;
|
||||
res = occurs_check_enter(app);
|
||||
break;
|
||||
|
||||
case EXIT:
|
||||
|
|
Loading…
Reference in a new issue