From ebce0b3612664fe34a13bed9d1db8f1a4c41afb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Jul 2020 14:40:45 -0700 Subject: [PATCH] fix #4577 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 555c1b5c2..1df3d85ab 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -691,16 +691,29 @@ expr_ref array_rewriter::expand_store(expr* s) { br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { TRACE("array_rewriter", tout << mk_bounded_pp(lhs, m(), 2) << " " << mk_bounded_pp(rhs, m(), 2) << "\n";); - expr* v = nullptr; + expr* v = nullptr, *w = nullptr; if (m_util.is_const(rhs) && is_lambda(lhs)) { std::swap(lhs, rhs); } + if (m_util.is_const(rhs) && m_util.is_store(lhs)) { + std::swap(lhs, rhs); + } + if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) { + result = m().mk_eq(v, w); + return BR_REWRITE1; + } if (m_util.is_const(lhs, v) && is_lambda(rhs)) { quantifier* lam = to_quantifier(rhs); expr_ref e(m().mk_eq(lam->get_expr(), v), m()); 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)) {