Search for a AND (NOT a), a OR (NOT a), when doing node creation. This is necessary...

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 13021980109262f9afa99b2a9da43a5d4746b8f1..e52ce5a94e46ba22ac3e05174f0a47a4e81f62d7 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -338,6 +338,10 @@ SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTVec &children)
       else
         next_it = it_end;
 
+      if (nextexists)
+        if (next_it->GetKind() == BEEV::NOT && (*next_it)[0] == *it)
+          return annihilator;
+
       if (*it == annihilator)
         {
           return annihilator;