summaryrefslogtreecommitdiff
path: root/src/theory/term_registration_visitor.cpp
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2012-05-27 00:38:30 +0000
committerClark Barrett <barrett@cs.nyu.edu>2012-05-27 00:38:30 +0000
commitcf640b735157b0f5d053a7b938ee452dcfd00c66 (patch)
tree43f145659d6fbec4c6c4718a4740ed43717a4014 /src/theory/term_registration_visitor.cpp
parentb5de553d4d7f588afaa02a2fb4311700f5f65761 (diff)
Another expensive function call in a Debug line
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r--src/theory/term_registration_visitor.cpp4
1 files changed, 3 insertions, 1 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback