cnf conversion

2 files changed, 8 insertions, 1 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 747854d23..13aa0b0ff 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -390,7 +390,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
   d_childrenStorage() {
 
   if(evIsAllocated(nb)) {
-    realloc(nb->d_size, false);
+    realloc(nb.d_size, false);
     std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
   } else {
     std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 985ad15a7..84df5957a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -29,6 +29,7 @@
 #include "kind.h"
 
 #include <string>
+#include <iterator>
 
 namespace CVC4 {
 
@@ -142,6 +143,12 @@ class NodeValue {
     node_iterator operator++(int) {
       return node_iterator(d_i++);
     }
+
+    typedef std::input_iterator_tag iterator_category;
+    typedef Node value_type;
+    typedef ptrdiff_t difference_type;
+    typedef Node* pointer;
+    typedef Node& reference;
   };
   typedef node_iterator const_node_iterator;