Work around rare problem caused by the simplifying node factory.

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

diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
index c2c8eecf534b47703254a03e1346eaa44cb37e2e..b7a21bc47739f6a3c50a0d6861207c0c9cdb90ea 100644 (file)
--- a/src/simplifier/MutableASTNode.h
+++ b/src/simplifier/MutableASTNode.h
@@ -119,18 +119,24 @@ private:
       for (int i = 0; i < children.size(); i++)
         newChildren.push_back(children[i]->toASTNode(nf));
 
+      // Don't use the hashing node factory here. Imagine CreateNode simplified down,
+      // from (= 1 ite( x , 1,0)) to x (say). Then this node will become a symbol,
+      // but, this object will still have the equal's children. i.e. 1, and the ITE.
+      // So it becomes a SYMBOL with children...
+
       if (n.GetType() == BOOLEAN_TYPE)
         {
-          n = nf->CreateNode(n.GetKind(), newChildren);
+          n = n.GetSTPMgr()->hashingNodeFactory->CreateNode(n.GetKind(), newChildren);
         }
       else if (n.GetType() == BITVECTOR_TYPE)
         {
-          n = nf->CreateTerm(n.GetKind(), n.GetValueWidth(), newChildren);
+          n = n.GetSTPMgr()->hashingNodeFactory->CreateTerm(n.GetKind(), n.GetValueWidth(), newChildren);
         }
       else
         {
-          n = nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), newChildren);
+          n = n.GetSTPMgr()->hashingNodeFactory->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), newChildren);
         }
+
       dirty = false;
       return n;
     }