From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 9 Sep 2013 18:41:21 +0000 (-0400)
Subject: Ensure no cost for datatypes debugging when not tracing it.
X-Git-Tag: cvc5-1.0.0~7287^2~25
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d565fae2a46460e92cb097760ce9f9a0954b1747;p=cvc5.git

Ensure no cost for datatypes debugging when not tracing it.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index cbbee4a14..9dc8c0028 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1082,6 +1082,10 @@ Node TheoryDatatypes::getRepresentative( Node a ){
 
 
 void TheoryDatatypes::printModelDebug( const char* c ){
+  if(! (Trace.isOn(c))) {
+    return;
+  }
+
   Trace( c ) << "Datatypes model : " << std::endl;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){