From f5840cd042274423d18a064d1bc99dca2b8ef16d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 5 Jan 2012 00:45:34 +0000 Subject: [PATCH] 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 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- 2.47.3