From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sun, 27 May 2012 00:38:30 +0000 (+0000)
Subject: Another expensive function call in a Debug line
X-Git-Tag: cvc5-1.0.0~8142
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf640b735157b0f5d053a7b938ee452dcfd00c66;p=cvc5.git

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 e1ef51d09..099871ceb 100644
--- 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);