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