1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3a6b6e15a..138a87493 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -473,6 +473,9 @@ public:
    */
   inline Type mkPredicateType(const std::vector<Type>& sorts);
 
+  /** Make a new sort. */
+  inline Type mkSort();
+
   /** Make a new sort with the given name. */
   inline Type mkSort(const std::string& name);
 
@@ -630,6 +633,10 @@ NodeManager::mkPredicateType(const std::vector<Type>& sorts) {
   return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
 }
 
+inline Type NodeManager::mkSort() {
+  return Type(this, mkVarPtr(kindType()));
+}
+
 inline Type NodeManager::mkSort(const std::string& name) {
   return Type(this, mkVarPtr(name, kindType()));
 }