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

Move out equality use out of the loop

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-04 12:42:39 -07:00
parent 0353fc38ff
commit 71fc83c051
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_datatype.cpp
View file

@ -551,11 +551,12 @@ namespace smt {
if (aarg->get_root() == child->get_root()) { if (aarg->get_root() == child->get_root()) {
if (aarg != child) if (aarg != child)
m_used_eqs.push_back(enode_pair(aarg, child)); m_used_eqs.push_back(enode_pair(aarg, child));
if (sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
found = true; found = true;
} }
} }
if (sibling && sibling != arg)
m_used_eqs.push_back(enode_pair(arg, sibling));
} }
} }
VERIFY(found); VERIFY(found);