Improvmeent. Speed up the division propagator a little.

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

diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
index bb485a809a67ae81a24f395a0df6f7070fccc68c..dea6eb196ad35cf2d21107f3c91b8350060e4807 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
@@ -402,21 +402,24 @@ Result bvUnsignedQuotientAndRemainder(vector<FixedBits*>& children,
                }
 
                {
-                       Result r1 = fix(a, minTop, maxTop);
-                       r1 = merge(r1,fix(a, minTop, maxTop));
+                Result r1 = fix(a, minTop, maxTop);
+                if (r1 == CHANGED)
+                  r1 = merge(r1,fix(a, minTop, maxTop));
+
+                Result r2 = fix(b, minBottom, maxBottom);
+                if (r2 == CHANGED) // We call is a second time because it's not idepotent..
+                  r2 = merge(r2,fix(b, minBottom, maxBottom));
+
+                Result r3;
+                if (whatIs == QUOTIENT_IS_OUTPUT)
+                  {
+                    r3 = fix(output, minQuotient, maxQuotient);
+                    if (r3 == CHANGED)
+                      r3 = merge(r3,fix(output, minQuotient, maxQuotient));
+                  }
+                else
+                        r3 = fix(output, minRemainder, maxRemainder);
 
-                       Result r2 = fix(b, minBottom, maxBottom);
-                       // We call is a second time because it's not idepotent..
-                       r2 = merge(r2,fix(b, minBottom, maxBottom));
-
-                       Result r3;
-                       if (whatIs == QUOTIENT_IS_OUTPUT)
-                         {
-                           r3 = fix(output, minQuotient, maxQuotient);
-                           r3 = merge(r3,fix(output, minQuotient, maxQuotient));
-                         }
-                       else
-                               r3 = fix(output, minRemainder, maxRemainder);
 
                        if (r1 == CONFLICT || r2 == CONFLICT || r3 == CONFLICT)
                        {