mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix #4848

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-07 05:59:55 -08:00
parent 27dac3e1a0
commit 6c9bdc949e
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -1317,7 +1317,7 @@ func_decl * model_value_decl_plugin::mk_func_decl(decl_kind k, unsigned num_para
int idx = parameters[0].get_int();
sort * s = to_sort(parameters[1].get_ast());
string_buffer<64> buffer;
buffer << s->get_name().bare_str() << "!val!" << idx;
buffer << s->get_name().str() << "!val!" << idx;
func_decl_info info(m_family_id, k, num_parameters, parameters);
info.m_private_parameters = true;
return m_manager->mk_func_decl(symbol(buffer.c_str()), 0, static_cast<sort * const *>(nullptr), s, info);