From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 May 2012 06:24:52 +0000 (+0000)
Subject: small improvement. Pull up bvnot from bvarshift.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ccecd9ed1a6550248e13d68523dda5b0201fd444;p=francis%2Fstp.git

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 f688209..4ff76b2 100644
--- 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;