small improvement. Pull up bvnot from bvarshift.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index f6882098a39c035544171f981c5cdadf0ebcbd57..4ff76b2639c09e98494010c9926cfaeac89e36cd 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -1026,8 +1026,9 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
       else if (children[0].isConstant() && !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(), width - 1))
         result = NodeFactory::CreateTerm(BVRIGHTSHIFT, width, children[0], children[1]);
       else if ( width >= 3 && children[0].GetKind() == BVNEG && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0] )
-        result =  NodeFactory::CreateTerm(BVSRSHIFT,width,children[0],children[0][0]);//414 -> 361
-
+              result =  NodeFactory::CreateTerm(BVSRSHIFT,width,children[0],children[0][0]);//414 -> 361
+      else if (children[0].GetKind() == BVNEG)
+        result =  NodeFactory::CreateTerm(BVNEG, width, NodeFactory::CreateTerm(BVSRSHIFT,width,children[0][0],children[1]));
 
     }
     break;