Slightly speed up the equals propagator.

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

diff --git a/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp
index 62338094d6a47f8576079fc4fa38ecd677a17d62..1846020e98f0ab71c4fa5206b690dc3b44bb5b60 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_TransferFunctions.cpp
@@ -40,6 +40,7 @@ Result bvEqualsBothWays(FixedBits& a, FixedBits& b, FixedBits& output)
                        if (a.getValue(i) != b.getValue(i))
                        {
                                definatelyFalse = true;
+                               break;
                        }
                        else
                        {
@@ -111,7 +112,7 @@ Result bvEqualsBothWays(FixedBits& a, FixedBits& b, FixedBits& output)
        {
                int unknown = 0;
 
-               for (int i = 0; i < childWidth; i++)
+               for (int i = 0; i < childWidth && unknown < 2; i++)
                {
                        if (!a.isFixed(i))
                                unknown++;