From b04e48f374e1e8b1bba3fef5f2a13c4bf2f25f53 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Aug 2023 15:06:39 -0700 Subject: [PATCH] fix #6850 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/pdecl.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index a64d0ede9..f343be94d 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -838,14 +838,18 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { } format * pp(smt2_pp_environment& env, pdecl_manager const & m) const override { + symbol s = m_decl->get_name(); + std::string name = s.str(); + if (is_smt2_quoted_symbol(s)) + name = mk_smt2_quoted_symbol(s); if (m_args.empty()) { - return mk_string(m.m(), m_decl->get_name().str()); + return mk_string(m.m(), name); } else { ptr_buffer b; for (auto arg : m_args) b.push_back(m.pp(env, arg)); - return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str()); + return mk_seq1(m.m(), b.begin(), b.end(), f2f(), name); } } }; @@ -874,12 +878,17 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { } format * pp(smt2_pp_environment& env, pdecl_manager const & m) const override { + symbol s = m_decl->get_name(); + std::string name = s.str(); + if (is_smt2_quoted_symbol(s)) + name = mk_smt2_quoted_symbol(s); + if (m_indices.empty()) { - return mk_string(m.m(), m_decl->get_name().str()); + return mk_string(m.m(), name); } else { ptr_buffer b; - b.push_back(mk_string(m.m(), m_decl->get_name().str())); + b.push_back(mk_string(m.m(), name)); for (auto idx : m_indices) b.push_back(mk_unsigned(m.m(), idx)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_");