From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 27 Apr 2011 07:10:09 +0000 (+0000)
Subject: Important Bugfix. The prior checkin causes the WRONG answer sometimes.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=02e9145da2a9d0446fd8630323db155f0dc06fb4;p=francis%2Fstp.git

Important Bugfix. The prior checkin causes the WRONG answer sometimes.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 05efa15..e0a7e8d 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -110,11 +110,8 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
             	result = ASTFalse;
 		}
 
-                if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][1] == children[1][1])
-                        result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][0], children[1][0]);
-
-                if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][0] == children[1][0])
-                        result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][1], children[1][1]);
+            if (children[0].GetKind() ==BEEV::BVCONCAT && children[1].GetKind() == BEEV::BVCONCAT && children[0][1] == children[1][1])
+                result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][0], children[1][0]);
 
 
 		break;