diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index efac34902..feec9b782 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -420,8 +420,15 @@ TypeNode NodeManager::getType(TNode n, bool check) Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl; - - if(needsCheck && !(*d_options)[options::earlyTypeChecking]) { + +#ifdef CVC4_DEBUG + // already did type check eagerly upon creation in node builder + bool doTypeCheck = false; +#else + bool doTypeCheck = true; +#endif + if (needsCheck && doTypeCheck) + { /* Iterate and compute the children bottom up. This avoids stack overflows in computeType() when the Node graph is really deep, which should only affect us when we're type checking lazily. */ |