mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

fix #6561

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-28 03:47:18 -08:00
parent 83bd3d1e21
commit 246d6f7b77
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tactic/core/reduce_args_tactic.cpp
View file

@ -398,9 +398,11 @@ struct reduce_args_tactic::imp {
var_ref_vector new_vars(m); var_ref_vector new_vars(m);
ptr_buffer<expr> new_eqs; ptr_buffer<expr> new_eqs;
generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args");
for (auto const& kv : decl2arg2funcs) { for (auto const& [f, map] : decl2arg2funcs)
func_decl * f = kv.m_key; for (auto const& [t, new_def] : *map)
arg2func * map = kv.m_value; f_mc->hide(new_def);
for (auto const& [f, map] : decl2arg2funcs) {
expr * def = nullptr; expr * def = nullptr;
SASSERT(decl2args.contains(f)); SASSERT(decl2args.contains(f));
bit_vector & bv = decl2args.find(f); bit_vector & bv = decl2args.find(f);
@ -412,7 +414,7 @@ struct reduce_args_tactic::imp {
new_args.push_back(new_vars.back()); new_args.push_back(new_vars.back());
} }
for (auto const& [t, new_def] : *map) { for (auto const& [t, new_def] : *map) {
f_mc->hide(new_def); // f_mc->hide(new_def);
SASSERT(new_def->get_arity() == new_args.size()); SASSERT(new_def->get_arity() == new_args.size());
app * new_t = m.mk_app(new_def, new_args); app * new_t = m.mk_app(new_def, new_args);
if (def == nullptr) { if (def == nullptr) {