mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Only print func-decl names for indexed parameters (#6663)
This commit is contained in:
parent
e0a066efa3
commit
6324db207b
|
@ -121,8 +121,10 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) {
|
||||||
std::string str = f->get_parameter(i).get_rational().to_string();
|
std::string str = f->get_parameter(i).get_rational().to_string();
|
||||||
fs.push_back(mk_string(get_manager(), str));
|
fs.push_back(mk_string(get_manager(), str));
|
||||||
}
|
}
|
||||||
else
|
else {
|
||||||
fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast())));
|
unsigned len;
|
||||||
|
fs.push_back(pp_fdecl_name(to_func_decl(f->get_parameter(i).get_ast()), len));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
return mk_seq1(get_manager(), fs.begin(), fs.end(), f2f(), "_");
|
return mk_seq1(get_manager(), fs.begin(), fs.end(), f2f(), "_");
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue