1 files changed, 4 insertions, 1 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 716e2a3b3..4cde0c624 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -238,7 +238,7 @@ void NodeManager::reclaimZombies() {
 }/* NodeManager::reclaimZombies() */
 
 TypeNode NodeManager::computeType(TNode n, bool check)
-  throw (TypeCheckingExceptionPrivate, AssertionException) {  
+  throw (TypeCheckingExceptionPrivate, AssertionException) {
   TypeNode typeNode;
 
   // Infer the type
@@ -444,6 +444,9 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   case kind::APPLY_TESTER:
     typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check);
     break;
+  case kind::APPLY_TYPE_ASCRIPTION:
+    typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check);
+    break;
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled(n.getKind());