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.

1 files changed, 4 insertions, 2 deletions

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);
     }