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 df1e2bb3e185b58c0a7c07f57d2416e9a66ee085..49537fa084dba3bf10c6de731f899f83c8697308 100644 (file)
--- 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 f7e97c8bac2b71d882b1b2f573777d40f26ef52e..796757dea9f9c626507db29a19027c0047da23e8 100644 (file)
--- 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;
   }