From 790b13d55098c21bb53a97475d5a78d90b5a2bc3 Mon Sep 17 00:00:00 2001 From: hgvk94 Date: Fri, 31 Mar 2023 19:45:07 -0400 Subject: [PATCH] Only print func-decl names for indexed parameters --- src/ast/ast_smt2_pp.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 74bb871ece4..bfa26241049 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -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(); fs.push_back(mk_string(get_manager(), str)); } - else - fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast()))); + else { + 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(), "_"); }