From b94d1607bfed1a66591a35de40d7d2a00014286c Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 27 May 2014 14:43:46 -0400
Subject: [PATCH] Revert "timespec printing bug"

This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
---
 src/main/options                | 3 ---
 src/prop/minisat/core/Solver.cc | 8 --------
 src/util/statistics_registry.h  | 4 ++--
 3 files changed, 2 insertions(+), 13 deletions(-)

diff --git a/src/main/options b/src/main/options
index 943f46b61..8733011f7 100644
--- a/src/main/options
+++ b/src/main/options
@@ -53,7 +53,4 @@ undocumented-alias --segv-nospin = --no-segv-spin
 expert-option waitToJoin --wait-to-join bool :default true
  wait for other threads to join before quitting
 
-expert-option periodicStatsInterval --periodic-stats int :default 0
- print total time we have been running every N decisions
-
 endmodule
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());
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index be4a71979..8246bfdd2 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -694,7 +694,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) {
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
   CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
   a.tv_sec -= b.tv_sec;
-  long nsec = long(a.tv_nsec) - long(b.tv_nsec);
+  long nsec = a.tv_nsec - b.tv_nsec;
   if(nsec < 0) {
     nsec += nsec_per_sec;
     --a.tv_sec;
@@ -762,7 +762,7 @@ inline bool operator>=(const timespec& a, const timespec& b) {
 inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
   // assumes t.tv_nsec is in range
   return os << t.tv_sec << "."
-            << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
+            << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 }
 
 namespace CVC4 {
-- 
2.30.2