diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c6aee3dea..ae6bdbd29 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -73,8 +73,7 @@ Node NodeManager::mkNode(Kind kind, const vector<Node>& children) { } Node NodeManager::mkVar(const Type* type, string name) { - Node n = NodeBuilder<>(this, VARIABLE); - n.setAttribute(TypeAttr(), type); + Node n = mkVar(type); n.setAttribute(VarNameAttr(), name); return n; } |