diff options
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 3a2aca571..27756da5b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,7 +28,6 @@ #include "expr/kind.h" #include "expr/metakind.h" -#include "expr/type.h" #include "util/Assert.h" #include "util/output.h" @@ -248,7 +247,7 @@ public: * Returns the type of this node. * @return the type */ - Type* getType() const; + Type getType() const; /** * Returns the kind of this node. @@ -640,7 +639,7 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) { if(ref_count) { d_nv->dec(); } else { - Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted(), + Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted() || NodeManager::currentNM()->inDestruction(), "TNode pointing to an expired NodeValue at destruction time"); } } @@ -815,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -Type* NodeTemplate<ref_count>::getType() const { +Type NodeTemplate<ref_count>::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); |