fix #4689

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast_smt2_pp.cpp

@@ -31,6 +31,15 @@ using namespace format_ns;
 #define MAX_INDENT   16
 #define SMALL_INDENT 2
 
+std::string ensure_quote(symbol const& s) {
+    std::string str;
+    if (is_smt2_quoted_symbol(s))
+        str = mk_smt2_quoted_symbol(s);
+    else
+        str = s.str();
+    return str;
+}
+
 format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bool is_skolem) const {
     ast_manager & m = get_manager();
     if (is_smt2_quoted_symbol(s)) {
@@ -430,6 +439,8 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx");
     }
+    std::string name = ensure_quote(s->get_name());
+    
     if (get_dtutil().is_datatype(s)) {
         unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
         if (sz > 0) {
@@ -437,10 +448,10 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
             for (unsigned i = 0; i < sz; i++) {
                 fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i)));
             }
-            return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str());
+            return mk_seq1(m, fs.begin(), fs.end(), f2f(), name);
         }
     }
-    return format_ns::mk_string(get_manager(), s->get_name().str());
+    return format_ns::mk_string(get_manager(), name);
 }
 
 typedef app_ref_vector format_ref_vector;
@@ -543,14 +554,6 @@ class smt2_printer {
     ast_manager & m() const { return m_manager; }
     ast_manager & fm() const { return format_ns::fm(m()); }
 
-    std::string ensure_quote(symbol const& s) {
-        std::string str;
-        if (is_smt2_quoted_symbol(s))
-            str = mk_smt2_quoted_symbol(s);
-        else
-            str = s.str();
-        return str;
-    }
 
     symbol ensure_quote_sym(symbol const& s) {
         if (is_smt2_quoted_symbol(s)) {

src/ast/ast_smt2_pp.h

@@ -33,6 +33,8 @@ Revision History:
 #include "ast/ast_smt_pp.h"
 #include "util/smt2_util.h"
 
+std::string ensure_quote(symbol const& s);
+
 class smt2_pp_environment {
 protected:
     mutable smt_renaming m_renaming;

src/ast/ast_smt_pp.cpp

@@ -801,7 +801,7 @@ public:
         bool first_def = true;
         for (datatype::def* d : defs) {
             if (!first_def) m_out << "\n    "; else first_def = false;
-            m_out << "(" << d->name() << " " << d->params().size() << ")";
+            m_out << "(" << ensure_quote(d->name()) << " " << d->params().size() << ")";
         }
         m_out << ") (";
         bool first_sort = true;