* When outputting runtimes with the -t flag, omit anything that has a zero milli...

* 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

diff --git a/scripts/run_cvc_tests.pl b/scripts/run_cvc_tests.pl
index b5dea9bde138992befc82c933100d333b01fcf04..366ce0e722c38efe3352a7eedb38d4f0ad576591 100755 (executable)
--- 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 24b42a479b5fde34b2b9c5a61e34468148714a95..3cee1a46a59efa84db19ebaa14c0649761474ef4 100644 (file)
--- 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