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

Update array_axioms.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-16 17:52:31 -07:00
parent 749d1ab305
commit 34fc0276e9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -176,7 +176,7 @@ namespace array {
unsigned num_args = select->get_num_args(); unsigned num_args = select->get_num_args();
expr* arg = select->get_arg(0); expr* arg = select->get_arg(0);
if (arg != store && !can_beta_reduce(arg) && expr2enode(arg)->get_root() == expr2enode(store)->get_root()) if (false && arg != store && !can_beta_reduce(arg) && expr2enode(arg)->get_root() == expr2enode(store)->get_root())
return false; 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++)