Improvement. run unconstrained elimination after propagating equalities. Unconstraine...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 69b01d6983c53cca954142f2a9fbf83bbf1711be..1fc735d73d020941a8a555030a1c7d90cbb0b1a4 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -112,14 +112,6 @@ namespace BEEV {
    ASTNode
   STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver)
   {
-    if (bm->UserFlags.isSet("enable-unconstrained", "1"))
-      {
-        // Remove unconstrained.
-        RemoveUnconstrained r1(*bm);
-        simplified_solved_InputToSAT = r1.topLevel(simplified_solved_InputToSAT, simp);
-        bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT);
-      }
-
     simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
     if (simp->hasUnappliedSubstitutions())
       {
@@ -128,6 +120,14 @@ namespace BEEV {
         bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
       }
 
+    if (bm->UserFlags.isSet("enable-unconstrained", "1"))
+      {
+        // Remove unconstrained.
+        RemoveUnconstrained r1(*bm);
+        simplified_solved_InputToSAT = r1.topLevel(simplified_solved_InputToSAT, simp);
+        bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT);
+      }
+
     if (bm->UserFlags.isSet("use-intervals", "1"))
       {
         EstablishIntervals intervals(*bm);