From: Tim King <taking@cs.nyu.edu>
Date: Tue, 1 Jun 2010 21:43:18 +0000 (+0000)
Subject: This commit adds a debugTagIsOn() guard around some extremely verbose debugging state... 
X-Git-Tag: cvc5-1.0.0~9012
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c0b0f4c42619d1de116dc73f2c5111fd27ea85c;p=cvc5.git

This commit adds a debugTagIsOn() guard around some extremely verbose debugging statements.  There is some evidence that these debugging statements were 20% of the running time for QF_LRA/miplib/fixnet-1000.smt in debug mode.
---

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 672675ac8..1dbf818b3 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -598,8 +598,10 @@ void TheoryArith::check(Effort level){
       //Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
-  if(fullEffort(level)){
-    for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
+  if(debugTagIsOn("model")){
+    for(vector<Node>::iterator i=d_variables.begin();
+        i!= d_variables.end();
+        ++i){
       Node var = *i;
       d_partialModel.printModel(var);
     }