From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 16 Feb 2010 18:24:00 +0000 (+0000)
Subject: removing assertion and warning that shouldn't be there. adding initialization of... 
X-Git-Tag: cvc5-1.0.0~9251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=094ffd30bf9f512d09e623d40329d4760852310b;p=cvc5.git

removing assertion and warning that shouldn't be there. adding initialization of kind to undefined to a default constructor.
---

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();