Fix for the last night's build errors (type that broke proper expression generation).

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 4bda235f5d2b40a19ffbf722fc04abaecd3f0b47..8243bd6da73a196ce27fc8ead6a4c36c3197cf26 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -864,14 +864,20 @@ inline Node NodeManager::mkNode(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
   Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED);
-  return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).append(children);
+  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  nb.append(children);
+  return nb;
 }
 
 template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).append(children).constructNodePtr();
+  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  nb.append(children);
+  return nb.constructNodePtr();
 }