From a083633ab437e00e64e0d58bcd069f201b2efcd6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Oct 2020 12:01:40 -0700
Subject: [PATCH] fix #4749

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_pp_util.cpp |  6 +++---
 src/ast/ast_smt_pp.cpp  | 18 ++++++++++++++++--
 src/ast/ast_smt_pp.h    |  1 +
 3 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
index 2e9a4114f..4b551ca6b 100644
--- a/src/ast/ast_pp_util.cpp
+++ b/src/ast/ast_pp_util.cpp
@@ -41,9 +41,9 @@ void ast_pp_util::display_decls(std::ostream& out) {
     bool first = m_num_decls == 0;
     coll.order_deps(m_num_sorts);
     unsigned n = coll.get_num_sorts();
-    for (unsigned i = m_num_sorts; i < n; ++i) {
-        pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr);
-    }
+    ast_mark seen;
+    for (unsigned i = m_num_sorts; i < n; ++i) 
+        pp.display_sort_decl(out, coll.get_sorts()[i], seen);
     m_num_sorts = n;
     n = coll.get_num_decls();
     for (unsigned i = m_num_decls; i < n; ++i) {
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 6e544c7af..53e928597 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -791,12 +791,18 @@ public:
         ptr_vector<datatype::def> defs;
         util.get_defs(s, defs);
 
+        unsigned j = 0;
         for (datatype::def* d : defs) {
             sort_ref sr = d->instantiate(ps);
-            if (mark.is_marked(sr)) return; // already processed
+            if (mark.is_marked(sr)) 
+                continue;
             mark.mark(sr, true);
+            defs[j++] = d;
         }
-
+        defs.shrink(j);
+        if (defs.empty())
+            return;
+        
         m_out << "(declare-datatypes (";
         bool first_def = true;
         for (datatype::def* d : defs) {
@@ -925,6 +931,14 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
     }
 }
 
+void ast_smt_pp::display_sort_decl(std::ostream& out, sort* s, ast_mark& seen) {
+    ptr_vector<quantifier> ql;
+    smt_renaming rn;
+    smt_printer p(out, m_manager, ql, rn, m_logic, false, m_simplify_implies, 0, 0, nullptr);
+    p.pp_sort_decl(seen, s);
+}
+
+
 
 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ptr_vector<quantifier> ql;
diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h
index c5242dc57..23b656c12 100644
--- a/src/ast/ast_smt_pp.h
+++ b/src/ast/ast_smt_pp.h
@@ -79,6 +79,7 @@ public:
     void display_smt2(std::ostream& strm, expr* n);
     void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
     void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
+    void display_sort_decl(std::ostream& out, sort* s, ast_mark& seen);
 
 };