From 71fc83c051b7a2163a46310f6ee74b972d7d8e6d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 4 Jul 2022 12:42:39 -0700
Subject: [PATCH] Move out equality use out of the loop

---
 src/smt/theory_datatype.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 358fda122..d11172691 100644
--- 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);