From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 1 May 2010 21:00:41 +0000 (+0000)
Subject: Fix for the last night's build errors (type that broke proper expression generation).
X-Git-Tag: cvc5-1.0.0~9091
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2da7b55f1a85cfc3fc2bc6abad16453c59d8c227;p=cvc5.git

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