2 files changed, 24 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b983c81f5..33322588f 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -112,4 +112,16 @@ bool NodeTemplate<ref_count>::isConst() const {
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
 
+template class NodeTemplate<true>;
+template class NodeTemplate<false>;
+
 }/* CVC4 namespace */
+
+namespace std {
+template class std::vector<CVC4::NodeTemplate<true>>;
+template class std::vector<CVC4::NodeTemplate<false>>;
+template class std::unordered_map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::NodeHashFunction>;
+template class std::unordered_map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false>, CVC4::TNodeHashFunction>;
+template class std::map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true> >;
+template class std::map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false> >;
+}
diff --git a/src/expr/node.h b/src/expr/node.h
index 4b12c7ece..8b21c7881 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1507,6 +1507,9 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
   return NodeManager::fromExpr(e);
 }
 
+extern template class NodeTemplate<true>;
+extern template class NodeTemplate<false>;
+
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
@@ -1568,4 +1571,13 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>&
 
 }/* CVC4 namespace */
 
+namespace std {
+extern template class std::vector<CVC4::NodeTemplate<true>>;
+extern template class std::vector<CVC4::NodeTemplate<false>>;
+extern template class std::unordered_map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::NodeHashFunction>;
+extern template class std::unordered_map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false>, CVC4::TNodeHashFunction>;
+extern template class std::map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true> >;
+extern template class std::map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false> >;
+}
+
 #endif /* __CVC4__NODE_H */