From 9c0b0f4c42619d1de116dc73f2c5111fd27ea85c Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 1 Jun 2010 21:43:18 +0000 Subject: [PATCH] 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(-) 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::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ + if(debugTagIsOn("model")){ + for(vector::iterator i=d_variables.begin(); + i!= d_variables.end(); + ++i){ Node var = *i; d_partialModel.printModel(var); } -- 2.30.2