From b0997661ccfccc76e66e00740ed53249d4bf8dcc Mon Sep 17 00:00:00 2001
From: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
Date: Mon, 19 Feb 2018 17:53:53 +0100
Subject: [PATCH] Insert sort declaration for nullary sorts declared using
 declare-datatype

---
 src/parsers/smt2/smt2parser.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 0b0420873..347cbbd68 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -970,6 +970,9 @@ namespace smt2 {
                 check_rparen_next("invalid datatype declaration, ')' expected");
             }
             else {
+                if (dt_name) {
+                    m_ctx.insert(pm().mk_psort_dt_decl(0, *dt_name));
+                }
                 parse_constructor_decls(ct_decls);
             }
             check_rparen_next("invalid datatype declaration, ')' expected");