mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

fix #6850

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-13 15:06:39 -07:00
parent 33c35b0c31
commit b04e48f374
1 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/cmd_context/pdecl.cpp
View file

@ -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 { 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()) { if (m_args.empty()) {
return mk_string(m.m(), m_decl->get_name().str()); return mk_string(m.m(), name);
} }
else { else {
ptr_buffer<format> b; ptr_buffer<format> b;
for (auto arg : m_args) for (auto arg : m_args)
b.push_back(m.pp(env, arg)); 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 { 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()) { if (m_indices.empty()) {
return mk_string(m.m(), m_decl->get_name().str()); return mk_string(m.m(), name);
} }
else { else {
ptr_buffer<format> b; ptr_buffer<format> 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) for (auto idx : m_indices)
b.push_back(mk_unsigned(m.m(), idx)); b.push_back(mk_unsigned(m.m(), idx));
return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_"); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_");