From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 29 Mar 2011 13:18:23 +0000 (+0000)
Subject: Work around rare problem caused by the simplifying node factory.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4c6bd006421318b094fb72134351ec72e74d2eef;p=francis%2Fstp.git

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 c2c8eec..b7a21bc 100644
--- 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;
     }