mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

cosmetic updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-23 18:49:38 -08:00
parent 85d3041a80
commit e332904fb2
1 changed files with 7 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.cpp
View file

@ -2167,16 +2167,14 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
if (decl == mk_func_decl(basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast<expr * const *>(nullptr))) if (decl == mk_func_decl(basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast<expr * const *>(nullptr)))
return r; return r;
*m_trace_stream << "[mk-proof] #"; *m_trace_stream << "[mk-proof] #";
} else { }
*m_trace_stream << "[mk-app] #"; else
} *m_trace_stream << "[mk-app] #";
*m_trace_stream << r->get_id() << " "; *m_trace_stream << r->get_id() << " ";
if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") { if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int")
ast_ll_pp(*m_trace_stream, *this, r); ast_ll_pp(*m_trace_stream, *this, r);
} else if (is_label_lit(r))
else if (is_label_lit(r)) { ast_ll_pp(*m_trace_stream, *this, r);
ast_ll_pp(*m_trace_stream, *this, r);
}
else { else {
*m_trace_stream << r->get_decl()->get_name(); *m_trace_stream << r->get_decl()->get_name();
for (unsigned i = 0; i < r->get_num_args(); i++) for (unsigned i = 0; i < r->get_num_args(); i++)