From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 29 Dec 2011 02:04:00 +0000 (+0000)
Subject: Refactor. Redoing the same changes in smaller pieces.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=667fb882631bf0d2c6113b6ad84871eef84c0cfd;p=francis%2Fstp.git

Refactor. Redoing the same changes in smaller pieces.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1448 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index df1e2bb..49537fa 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -28,7 +28,7 @@ public:
       BitBlasting, 
       Solving, 
       BVSolver, 
-      CreateSubstitutionMap, 
+      PropagateEqualities, 
       SendingToSAT,
       CounterExampleGeneration,
       SATSimplifying,
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index f7e97c8..796757d 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -124,9 +124,9 @@ namespace BEEV
   ASTNode
   Simplifier::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer* at)
   {
-    _bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
+    _bm->GetRunTimes()->start(RunTimes::PropagateEqualities);
     ASTNode result = substitutionMap.CreateSubstitutionMap(a, at);
-    _bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
+    _bm->GetRunTimes()->stop(RunTimes::PropagateEqualities);
     return result;
   }