From b8bb85a0d0ca254081f216481974deed9d449aa5 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 22 Dec 2020 15:17:27 -0800 Subject: [PATCH] Delete duplicated code (#5718) --- src/theory/term_registration_visitor.cpp | 16 ---------------- 1 file changed, 16 deletions(-) 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 -- 2.30.2