From 3d13c0335f2fc30239b5438910ababf023bc56a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Aug 2021 18:40:05 -0700 Subject: [PATCH] #5454 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_axioms.cpp | 6 +----- src/sat/smt/array_solver.cpp | 7 ++----- 2 files changed, 3 insertions(+), 10 deletions(-) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 2e8a0603d..372e05c75 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -175,18 +175,14 @@ namespace array { ptr_buffer sel1_args, sel2_args; unsigned num_args = select->get_num_args(); - if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) - return false; bool has_diff = false; for (unsigned i = 1; i < num_args; i++) has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root(); if (!has_diff) return false; - sel1_args.push_back(store); - sel2_args.push_back(store->get_arg(0)); - + sel2_args.push_back(store->get_arg(0)); for (unsigned i = 1; i < num_args; i++) { sel1_args.push_back(select->get_arg(i)); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index b56f4efb1..47ccfcc62 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -228,11 +228,8 @@ namespace array { auto& d = get_var_data(v); - for (euf::enode* lambda : d.m_lambdas) { - expr* e = lambda->get_expr(); - if (a.is_const(e) || a.is_map(e)) - propagate_select_axioms(d, lambda); - } + for (euf::enode* lambda : d.m_lambdas) + propagate_select_axioms(d, lambda); for (euf::enode* lambda : d.m_parent_lambdas) propagate_select_axioms(d, lambda);