Another expensive function call in a Debug line

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index e1ef51d0920532f62f7281c525761aa56ef53802..099871ceb20fa0855f570db488a96d41f606f902 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -171,7 +171,9 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 
   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
-  Debug("register::internal") << toString() << std::endl;
+  if (Debug.isOn("register::internal")) {
+    Debug("register::internal") << toString() << std::endl;
+  }
 
   // Get the theories of the terms
   TheoryId currentTheoryId = Theory::theoryOf(current);