summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-09-09 14:41:21 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-09-09 17:21:41 -0400
commitd565fae2a46460e92cb097760ce9f9a0954b1747 (patch)
treec9560a95610392f0de034257c3fcbb3e47f02d8d
parentcd30c0c2fa324abfe6e29cad8d0a1710fc484607 (diff)
Ensure no cost for datatypes debugging when not tracing it.
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp4
1 files changed, 4 insertions, 0 deletions
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() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback