Move out equality use out of the loop

Z3Prover · Jul 4, 2022 · 71fc83c · 71fc83c
1 parent 0353fc3
commit 71fc83c
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
@@ -551,11 +551,12 @@ namespace smt {
                     if (aarg->get_root() == child->get_root()) {
                         if (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;
                     }
                 }
+                if (sibling && sibling != arg)
+                    m_used_eqs.push_back(enode_pair(arg, sibling));
+
             }
         }
         VERIFY(found);