1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 2d96ac57a..7e0cfd0cf 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -313,6 +313,8 @@ public:
   Node mkVar(const TypeNode& type);
   Node* mkVarPtr(const TypeNode& type);
 
+  /** Create a skolem constant with the given type. */
+  Node mkSkolem(const TypeNode& type);
 
   /**
    * Create a constant of type T.  It will have the appropriate
@@ -864,6 +866,12 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   return n;
 }
 
+inline Node NodeManager::mkSkolem(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::SKOLEM);
+  n.setAttribute(TypeAttr(), type);
+  return n;
+}
+
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   return mkConstInternal<Node, T>(val);