mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5454

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-15 18:40:05 -07:00
parent 6a3ba64afe
commit 3d13c0335f
2 changed files with 3 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/array_axioms.cpp
View file

@ -175,18 +175,14 @@ namespace array {
ptr_buffer<expr> sel1_args, sel2_args; ptr_buffer<expr> sel1_args, sel2_args;
unsigned num_args = select->get_num_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; bool has_diff = false;
for (unsigned i = 1; i < num_args; i++) for (unsigned i = 1; i < num_args; i++)
has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root(); has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
if (!has_diff) if (!has_diff)
return false; return false;
sel1_args.push_back(store); 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++) { for (unsigned i = 1; i < num_args; i++) {
sel1_args.push_back(select->get_arg(i)); sel1_args.push_back(select->get_arg(i));

7
src/sat/smt/array_solver.cpp
View file

@ -228,11 +228,8 @@ namespace array {
auto& d = get_var_data(v); auto& d = get_var_data(v);
for (euf::enode* lambda : d.m_lambdas) { for (euf::enode* lambda : d.m_lambdas)
expr* e = lambda->get_expr(); propagate_select_axioms(d, lambda);
if (a.is_const(e) || a.is_map(e))
propagate_select_axioms(d, lambda);
}
for (euf::enode* lambda : d.m_parent_lambdas) for (euf::enode* lambda : d.m_parent_lambdas)
propagate_select_axioms(d, lambda); propagate_select_axioms(d, lambda);