From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 27 Oct 2010 22:53:09 +0000 (+0000)
Subject: Small change to documentation in NodeManager::getType
X-Git-Tag: cvc5-1.0.0~8767
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be432fe60ee4bd7ae9143a38c7a4f30ad47c5eda;p=cvc5.git

Small change to documentation in NodeManager::getType
---

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index b0592ba2f..2f5ba6824 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -430,15 +430,17 @@ TypeNode NodeManager::getType(TNode n, bool check)
     stack<TNode> worklist;
     worklist.push(n);
 
-    /* Iterate and compute the children bottom up. */
+    /* Iterate and compute the children bottom up. This avoids stack
+       overflows in computeType() when the Node graph is really
+       deep. */
     while( !worklist.empty() ) {
       TNode m = worklist.top();
 
       bool readyToCompute = true;
-      TNode::iterator it = m.begin();
-      TNode::iterator end = m.end();
 
-      for( ; it != end; ++it ) {
+      for( TNode::iterator it = m.begin(), end = m.end() ; 
+           it != end; 
+           ++it ) {
         if( !hasAttribute(*it, TypeAttr()) 
             || (check && !getAttribute(*it, TypeCheckedAttr())) ) {
           readyToCompute = false;