From 582af96228b52a32ea4d9772b1820191e15ea1ab Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 12 May 2010 14:07:36 +0000
Subject: [PATCH] First attempt at tracking time spent building the counter
 example. Doesn't properly include abstraction refinement checking time (I
 think). This introduces changes from r316

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@760 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/RunTimes.cpp                            | 2 +-
 src/AST/RunTimes.h                              | 3 ++-
 src/absrefine_counterexample/CounterExample.cpp | 5 ++++-
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 3cee1a4..d564e09 100644
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include "RunTimes.h"
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation"};
 
 namespace BEEV
 {
diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 9f1ff00..20ccd3b 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -27,7 +27,8 @@ public:
       Solving, 
       BVSolver, 
       CreateSubstitutionMap, 
-      SendingToSAT
+      SendingToSAT,
+      CounterExampleGeneration
     };
 
   static std::string CategoryNames[];
diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 00bb674..e4ab1d0 100644
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -955,7 +955,8 @@ namespace BEEV
       }
     else if (SatSolver.okay())
       {
-        CounterExampleMap.clear();
+    	bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration);
+    	CounterExampleMap.clear();
         ConstructCounterExample(SatSolver);
         if (bm->UserFlags.stats_flag 
             && bm->UserFlags.print_nodes_flag)
@@ -971,6 +972,8 @@ namespace BEEV
           FatalError("TopLevelSat: Original input must compute to "\
                      "true or false against model");
 
+        bm->GetRunTimes()->stop(RunTimes::CounterExampleGeneration);
+
         // if the counterexample is indeed a good one, then return
         // invalid
         if (ASTTrue == orig_result)
-- 
2.47.3