Fix. I thought that extracts don't add any information but they do, if the underlying...

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

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 05d970ecc0d56228d642dbba9c509f9cb0601806..2b929b832a22b6d2b39146377afc8c3b5b5f4760 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -127,8 +127,8 @@ namespace simplifier
           if (node.isConstant())
               continue;
 
-          // other nodes will contain the same information (the extract doesn't change the fixings).
-          if (BVEXTRACT == node.GetKind() || BVCONCAT == node.GetKind())
+          // Concat doesn't change the fixings. Ignore it.
+          if (BVCONCAT == node.GetKind())
             continue;
 
           if (bits.isTotallyFixed())