diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-12-22 15:17:27 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-22 17:17:27 -0600 |
commit | b8bb85a0d0ca254081f216481974deed9d449aa5 (patch) | |
tree | b04f67c8f117c4e9cab55846677663a5a0b1bacb /src/theory/term_registration_visitor.cpp | |
parent | 2f73122d32e3272b1a9727857b6ac02d2da871d3 (diff) |
Delete duplicated code (#5718)
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 16 |
1 files changed, 0 insertions, 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 @@ -238,22 +238,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } } - 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 (TheoryIdSetUtil::setContains(currentTheoryId, theories)) { |