From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 27 Apr 2011 01:33:46 +0000 (+0000)
Subject: Fix. I thought that extracts don't add any information but they do, if the underlying... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6c385d039af78db032a6dffdf5a9d202ca9eb6e8;p=francis%2Fstp.git

Fix. I thought that extracts don't add any information but they do, if the underlying term has only partial fixed information.

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 05d970e..2b929b8 100644
--- 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())