1 files changed, 16 insertions, 0 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5d80dd55f..a5ce1bed0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -563,6 +563,22 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   {
     t = d_solver->mkEmptySet(s);
   }
+  else if (k == api::CONST_SEQUENCE)
+  {
+    if (!s.isSequence())
+    {
+      std::stringstream ss;
+      ss << "Type ascription on empty sequence must be a sequence, got " << s;
+      parseError(ss.str());
+    }
+    if (!t.getConstSequenceElements().empty())
+    {
+      std::stringstream ss;
+      ss << "Cannot apply a type ascription to a non-empty sequence";
+      parseError(ss.str());
+    }
+    t = d_solver->mkEmptySequence(s.getSequenceElementSort());
+  }
   else if (k == api::UNIVERSE_SET)
   {
     t = d_solver->mkUniverseSet(s);