Fix erroneous results when the logic was incorrectly specified (by throwing LogicException). Also correct a case where sharing was doing some work during pure theory solving.

1 files changed, 0 insertions, 9 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 48d00130c..558975a72 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -127,15 +127,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   Assert(alreadyVisited(current, parent));
 }
 
-void PreRegisterVisitor::start(TNode node) {
-  d_multipleTheories = false;
-}
-
-bool PreRegisterVisitor::done(TNode node) {
-  // We have multiple theories if removing the node theory from others is non-empty
-  return Theory::setRemove(Theory::theoryOf(node), d_theories);
-}
-
 std::string SharedTermsVisitor::toString() const {
   std::stringstream ss;
   TNodeVisitedMap::const_iterator it = d_visited.begin();