From 9c0b0f4c42619d1de116dc73f2c5111fd27ea85c Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 1 Jun 2010 21:43:18 +0000
Subject: 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.

---
 src/theory/arith/theory_arith.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/theory')

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);
     }
-- 
cgit v1.2.3