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

formatting updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-05-02 12:17:32 -07:00
parent 392266c278
commit c64d61bd0a
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/model/model_smt2_pp.cpp
View file

@ -195,12 +195,10 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
ptr_buffer<func_decl> func_decls; ptr_buffer<func_decl> func_decls;
sort_fun_decls(m, md, func_decls); sort_fun_decls(m, md, func_decls);
for (func_decl * f : func_decls) { for (func_decl * f : func_decls) {
if (recfun_util.is_defined(f) && !recfun_util.is_generated(f)) { if (recfun_util.is_defined(f) && !recfun_util.is_generated(f))
continue; continue;
} if (!m.is_considered_uninterpreted(f))
if (!m.is_considered_uninterpreted(f)) {
continue; continue;
}
func_interp * f_i = md.get_func_interp(f); func_interp * f_i = md.get_func_interp(f);
SASSERT(f->get_arity() == f_i->get_arity()); SASSERT(f->get_arity() == f_i->get_arity());
format_ref body(fm(m)); format_ref body(fm(m));