From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 22 Dec 2020 23:17:27 +0000 (-0800)
Subject: Delete duplicated code (#5718)
X-Git-Tag: cvc5-1.0.0~2409
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8bb85a0d0ca254081f216481974deed9d449aa5;p=cvc5.git

Delete duplicated code (#5718)
---

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 471a94e25..b4ad87f1e 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -222,22 +222,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
   bool useType = false;
   TheoryId typeTheoryId = THEORY_LAST;
 
-  if (current != parent) {
-    if (currentTheoryId != parentTheoryId) {
-      // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
-      TypeNode type = current.getType();
-      useType = true;
-      typeTheoryId = Theory::theoryOf(type);
-    } else {
-      TypeNode type = current.getType();
-      typeTheoryId = Theory::theoryOf(type);
-      if (typeTheoryId != currentTheoryId) {
-        if (type.isInterpretedFinite()) {
-          useType = true;
-        }
-      }
-    }
-  }
   if (current != parent) {
     if (currentTheoryId != parentTheoryId) {
       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers