Revert "timespec printing bug"

This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.

diff --git a/src/main/options b/src/main/options
index 943f46b61eff24ea8717a74aabbe430bf80989d4..8733011f7a2e456598affd00ce3b3415fc14fc8e 100644 (file)
--- 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 b2857216de94a9e2d08bbb23bf636839deed8ce9..610023b70387e480c4b86cffff50c7479d33d30e 100644 (file)
--- 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 be4a719792a4ab28fe3e8297d0c9aa4fdfae6f36..8246bfdd23c0aafdcf957e2e04f8dfee0353b7ef 100644 (file)
--- 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 {