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 98276fc7c56c1d9eb7cd35eaacfd527d4662ce39..41ff652c116212a140352058b17b9d01ea4d72b5 100644 (file)
--- 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;