diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-16 18:24:00 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-16 18:24:00 +0000 |
commit | 094ffd30bf9f512d09e623d40329d4760852310b (patch) | |
tree | e7151d2ac42dd07bb24d8ae5f83f01e0cd6f783b | |
parent | f795c7cc47d6932db14e6956f8c8fa687ab91859 (diff) |
removing assertion and warning that shouldn't be there. adding initialization of kind to undefined to a default constructor.
-rw-r--r-- | src/expr/node_builder.h | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index ce56fc08c..08a879600 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -455,7 +455,9 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) : d_used(false), d_ev(&d_inlineEv), d_inlineEv(0), - d_childrenStorage() {} + d_childrenStorage() { + d_inlineEv.d_kind = UNDEFINED_KIND; +} template <unsigned nchild_thresh> inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : @@ -474,8 +476,8 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : template <unsigned nchild_thresh> inline NodeBuilder<nchild_thresh>::~NodeBuilder() { if(!d_used) { - Warning("NodeBuilder unused at destruction\n"); - + // Warning("NodeBuilder unused at destruction\n"); + // Commented above, as it happens a lot, for example with exceptions dealloc(); } } @@ -547,9 +549,6 @@ inline void NodeBuilder<nchild_thresh>::dealloc() { * production; these are just sanity checks for debug builds */ Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used"); - Assert(evIsAllocated(), - "Internal error: NodeBuilder: " - "dealloc() called with stack-allocated NodeBuilder"); for(iterator i = d_ev->ev_begin(); i != d_ev->ev_end(); |