fixed timer issuerefactor_pp_backup

3 files changed, 3 insertions, 12 deletions

diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h
index 4831fe281..b25d02cff 100644
--- a/src/preproc/preprocessing_pass.h
+++ b/src/preproc/preprocessing_pass.h
@@ -66,7 +66,7 @@ public:
   size_t size() const { return d_nodes.size(); }
 
   void resize(size_t n) { d_nodes.resize(n); }
-  void clear() { d_nodes.clear(); }
+  void clear() { d_iteSkolemMap.clear(); d_nodes.clear(); }
 
   Node& operator[](size_t i) { return d_nodes[i]; }
   const Node& operator[](size_t i) const { return d_nodes[i]; }
@@ -130,10 +130,8 @@ class PreprocessingPass {
 
   PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) 
   {
-    if(!d_timerRunning) {    
+  //  if(!d_initialized) {
       TimerStat::CodeTimer simpITETimer(d_timer);
-      d_timerRunning = true;
-    }
     Trace("simplify") << "preproc::" << d_name << std::endl;
     Chat() << d_name << "..." << std::endl;
     dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
@@ -192,7 +190,7 @@ class PreprocessingPass {
   // have two different subclasses of PreprocessingPass or a superclass for
   // PreprocessingPass that does not do any registration.
 
- PreprocessingPass(const std::string& name, bool registerPass = false) : d_name(name), d_timer("preproc::" + name), d_initialized(false), d_timerRunning(false){
+ PreprocessingPass(const std::string& name, bool registerPass = false) : d_name(name), d_timer("preproc::" + name), d_initialized(false){
    if (registerPass) {
      PreprocessingPassRegistry::getInstance()->registerPass(name, this);
    }
@@ -227,7 +225,6 @@ protected:
   std::string d_name;
   TimerStat d_timer; 
   bool d_initialized;
-  bool d_timerRunning;
 };
 
 }  // namespace preproc
diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index a989b4a44..2f584a2ba 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -1126,10 +1126,7 @@ void DoStaticLearningPass::staticLearning(AssertionPipeline* assertionsToPreproc
   d_smt->finalOptionsAreSet();
   spendResource(options::preprocessStep());
 
-  TimerStat::CodeTimer staticLearningTimer(d_timer);
-
   Trace("simplify") << "SmtEnginePrivate::staticLearning()" << std::endl;
-
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
 
     NodeBuilder<> learned(kind::AND);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b7817d968..109d849b9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -623,7 +623,6 @@ public:
    * someone does a push-assert-pop without a check-sat.
    */
   void notifyPop() {
-    d_assertions.getSkolemMap()->clear();
     d_assertions.clear();
     d_nonClausalLearnedLiterals.clear();
     d_assertions.setRealAssertionsEnd(0);
@@ -2612,8 +2611,6 @@ void SmtEnginePrivate::processAssertions() {
  }
 
   d_assertionsProcessed = true;
-
-  d_assertions.getSkolemMap()->clear();
   d_assertions.clear();
 }