diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:43:46 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:43:46 -0400 |
| commit | b94d1607bfed1a66591a35de40d7d2a00014286c (patch) | |
| tree | fde01814a34288421b460901bed21fda6b73de1c /src/prop | |
| parent | 9006b759cfa01c6006196e0716c2d67c760556a6 (diff) | |
Revert "timespec printing bug"
This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b2857216d..610023b70 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -29,7 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/minisat.h" #include "prop/options.h" #include "util/output.h" -#include "util/periodic_statistics.h" #include "expr/command.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" @@ -479,13 +478,6 @@ Lit Solver::pickBranchLit() { Lit nextLit; - // Every so-many-decisions print the total time - if(options::periodicStatsInterval() && decisions % options::periodicStatsInterval() == 0) { - PeriodicStatistic::print("sat::decisions", decisions); - PeriodicStatistic::print("sat::conflicts", conflicts); - PeriodicStatistic::print("sat::propagations", propagations); - } - #ifdef CVC4_REPLAY nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); |