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 05efa15d4883c5484bf3a8b962bb378ff7928191..e0a7e8d2006f73803ad6d23d91a7679943b42d7e 100644 (file)
--- 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;