mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

remove unsound rewrite #4778

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-08 17:48:51 -08:00
parent e2c1436cc8
commit 864eaf8bf8
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -709,12 +709,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
return BR_REWRITE2;
}
if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
expr_ref eq1(m().mk_eq(v, to_app(rhs)->get_arg(to_app(rhs)->get_num_args()-1)), m());
expr_ref eq2(m().mk_eq(lhs, to_app(rhs)->get_arg(0)), m());
result = m().mk_and(eq1, eq2);
return BR_REWRITE3;
}
expr_ref lh1(m()), rh1(m());
if (m_expand_nested_stores) {
if (is_expandable_store(lhs)) {