mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

#5778 ensure else value so that defaults align across equivalence class

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-06 07:58:19 +02:00
parent ac2523af82
commit cebbc71330
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -116,6 +116,12 @@ namespace array {
if (!get_else(v) && fi->get_else()) if (!get_else(v) && fi->get_else())
set_else(v, fi->get_else()); set_else(v, fi->get_else());
if (!get_else(v)) {
expr* else_value = mdl.get_some_value(get_array_range(srt));
fi->set_else(else_value);
set_else(v, else_value);
}
for (euf::enode* p : *get_select_set(n)) { for (euf::enode* p : *get_select_set(n)) {
expr* value = values.get(p->get_root_id(), nullptr); expr* value = values.get(p->get_root_id(), nullptr);
if (!value || value == fi->get_else()) if (!value || value == fi->get_else())