mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
This commit is contained in:
parent
4da930b490
commit
9e5b6e0c9c
|
@ -556,7 +556,7 @@ namespace array {
|
|||
bool has_default = false;
|
||||
for (euf::enode* p : euf::enode_parents(n))
|
||||
has_default |= a.is_default(p->get_expr());
|
||||
if (has_default)
|
||||
if (!has_default)
|
||||
propagate_parent_default(v);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue