From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 5 Jan 2012 00:45:34 +0000 (+0000)
Subject: Important Bugfix. Thanks to Khoo Yit Phang.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f5840cd042274423d18a064d1bc99dca2b8ef16d;p=francis%2Fstp.git

Important Bugfix. Thanks to Khoo Yit Phang.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 98276fc..41ff652 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -1345,7 +1345,7 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
       result = NodeFactory::CreateTerm(ITE, width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)),
           bm.CreateOneConst(width), bm.CreateZeroConst(width));
     if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst()))
-      result = NodeFactory::CreateTerm(BVUMINUS, width, children[1]);
+      result = NodeFactory::CreateTerm(BVUMINUS, width, children[0]);
     else if (translate_signed)
       result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm);
     break;