diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 1d3e96f08..40e3e532f 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -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); return BR_DONE; case l_false: { - expr* arg0 = args[0]; - expr* arg1 = to_app(arg0)->get_arg(0); -#if 0 - IF_VERBOSE(0, verbose_stream() << mk_pp(arg0, m()) << "\n"); - while (m_util.is_store(arg1) && compare_args(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); + expr* arg0 = to_app(args[0])->get_arg(0); + while (m_util.is_store(arg0) && compare_args(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) { + arg0 = to_app(arg0)->get_arg(0); } -#endif // select(store(a, I, v), J) --> select(a, J) if I != J ptr_buffer new_args; - new_args.push_back(arg1); + new_args.push_back(arg0); new_args.append(num_args-1, args+1); result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data()); return BR_REWRITE1;