From 51a56904815209ca6fdb2a1b9dc697cbf61bc2e1 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 2 Mar 2010 12:53:46 +0000
Subject: [PATCH] * When outputting runtimes with the -t flag, omit anything
 that has a zero milli-second runtime. * Output the runtimes when performing a
 CVC regression test.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@624 e59a4935-1847-0410-ae03-e826735625c1
---
 scripts/run_cvc_tests.pl |  4 ++--
 src/AST/RunTimes.cpp     | 21 ++++++++++++++-------
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/scripts/run_cvc_tests.pl b/scripts/run_cvc_tests.pl
index b5dea9b..366ce0e 100755
--- a/scripts/run_cvc_tests.pl
+++ b/scripts/run_cvc_tests.pl
@@ -67,7 +67,7 @@ my %optionsDefault = ("level" => 4,
 		      "proofs" => 0,
 		      "lang" => "all",
 		      "stppath" => "stp/bin",
-		      "vc" => $pwd . "/bin/stp -d", # Program names
+		      "vc" => $pwd . "/bin/stp -d -t", # Program names
 		      #"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names
 		      "pfc" => "true",
 		      "stptestpath" => "stp/test",
@@ -78,7 +78,7 @@ my %optionsDefault = ("level" => 4,
 		      # Runtime limit; 0 = no limit
 		      "time" => 180,
 		      # Additional command line options to stp
-		      "stpOptions" => "-d");
+		      "stpOptions" => "-d -t");
 
 # Database of command line options.  Initially, they are undefined
 my %options = ();
diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 24b42a4..3cee1a4 100644
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -45,13 +45,20 @@ void RunTimes::print()
   std::map<Category, long>::const_iterator it2 = times.begin();
 
   while (it1 != counts.end())
-    {
-      result << " " << CategoryNames[it1->first] << ": " << it1->second;
-      if ((it2 = times.find(it1->first)) != times.end())
-        result << " [" << it2->second << "ms]";
-      result << std::endl;
-      it1++;
-    }
+  	{
+  		int time_ms = 0;
+  		if ((it2 = times.find(it1->first)) != times.end())
+  			time_ms = it2->second;
+
+  		if (time_ms!=0)
+  		{
+  			result << " " << CategoryNames[it1->first] << ": " << it1->second;
+  			result << " [" << time_ms << "ms]";
+  			result << std::endl;
+  		}
+  		it1++;
+  	}
+
 
   std::cerr << result.str();
   // iterator
-- 
2.47.3