1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 04de81b1c..117497539 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -974,6 +974,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
+  n.setAttribute(TypeAttr(), type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
 }
@@ -981,6 +982,7 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
   Node* n = mkVarPtr(type);
+  n->setAttribute(TypeAttr(), type);
   n->setAttribute(expr::VarNameAttr(), name);
   return n;
 }