1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8f7196e0c..2e45fe9d0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -190,6 +190,9 @@ TypeNode NodeManager::getType(TNode n)
   if(!hasType) {
     // Infer the type
     switch(n.getKind()) {
+    case kind::SORT_TYPE:
+      typeNode = kindType();
+      break;
     case kind::EQUAL:
       typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n);
       break;