From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 4 May 2011 05:04:31 +0000 (+0000)
Subject: Replace variables before calling the interval analysis.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f677b02c2a2951d5d222bce47f26ab9ee2a77587;p=francis%2Fstp.git

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 1c5478f..7cfd170 100644
--- 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);