mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix bug in array rewriter introduced in 202ce1e

Browse source
This commit is contained in:
Nuno Lopes 2022-06-21 22:40:40 +01:00
parent 36a1f758bc
commit 41deed59a3
1 changed files with 4 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/array_rewriter.cpp
View file

@ -174,21 +174,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
result = to_app(args[0])->get_arg(num_args); result = to_app(args[0])->get_arg(num_args);
return BR_DONE; return BR_DONE;
case l_false: { case l_false: {
expr* arg0 = args[0]; expr* arg0 = to_app(args[0])->get_arg(0);
expr* arg1 = to_app(arg0)->get_arg(0); while (m_util.is_store(arg0) && compare_args<true>(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
#if 0 arg0 = to_app(arg0)->get_arg(0);
IF_VERBOSE(0, verbose_stream() << mk_pp(arg0, m()) << "\n");
while (m_util.is_store(arg1) && compare_args<true>(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
IF_VERBOSE(0, verbose_stream() << "diff: " << mk_pp(arg1, m()) << "\n");
arg0 = arg1;
arg1 = to_app(arg0)->get_arg(0);
} }
#endif
// select(store(a, I, v), J) --> select(a, J) if I != J // select(store(a, I, v), J) --> select(a, J) if I != J
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
new_args.push_back(arg1); new_args.push_back(arg0);
new_args.append(num_args-1, args+1); new_args.append(num_args-1, args+1);
result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data()); result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data());
return BR_REWRITE1; return BR_REWRITE1;