Replace variables before calling the interval analysis.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 1c5478fce37bde1b28117df7f64a791a615d4c70..7cfd1705cc3943b8bd2c85a61b74e2d34df51cdf 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -99,13 +99,6 @@ namespace BEEV {
         bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT);
       }
 
-    if (bm->UserFlags.isSet("use-intervals", "1"))
-      {
-        EstablishIntervals intervals(*bm);
-        simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT);
-        bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT);
-      }
-
     simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
     if (simp->hasUnappliedSubstitutions())
       {
@@ -114,6 +107,13 @@ namespace BEEV {
         bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
       }
 
+    if (bm->UserFlags.isSet("use-intervals", "1"))
+      {
+        EstablishIntervals intervals(*bm);
+        simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT);
+        bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT);
+      }
+
     if (bm->UserFlags.bitConstantProp_flag)
       {
         bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);