From 2da7b55f1a85cfc3fc2bc6abad16453c59d8c227 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Sat, 1 May 2010 21:00:41 +0000
Subject: [PATCH] Fix for the last night's build errors (type that broke proper
 expression generation).

---
 src/expr/node_manager.h | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 4bda235f5..8243bd6da 100644
--- 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();
 }
 
 
-- 
2.30.2