mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

#5427

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-22 13:35:54 -07:00
parent 2589f2bad4
commit 848a8ebb98
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/array_internalize.cpp
View file

@ -177,6 +177,8 @@ namespace array {
auto set_index = [&](euf::enode* arg) { if (arg->get_root() == r) is_index = true; };
auto set_value = [&](euf::enode* arg) { if (arg->get_root() == r) is_value = true; };
if (a.is_ext(n->get_expr()))
return true;
for (euf::enode* parent : euf::enode_parents(r)) {
app* p = parent->get_app();
unsigned num_args = parent->num_args();
@ -193,7 +195,7 @@ namespace array {
}
else if (a.is_const(p)) {
set_value(parent->get_arg(0));
}
}
if (is_array + is_index + is_value > 1)
return true;
}