diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-01 21:00:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-01 21:00:41 +0000 |
commit | 2da7b55f1a85cfc3fc2bc6abad16453c59d8c227 (patch) | |
tree | c8da9119c0d60768b197a53b755f1d10aa56aa07 /src/expr/node_manager.h | |
parent | 592738efcfa12734e2ac0bb7e7dfa33299f1abb3 (diff) |
Fix for the last night's build errors (type that broke proper expression generation).
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 10 |
1 files 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(); } |