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

fix #5090

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-15 17:02:38 -07:00
parent ff0de59a70
commit ee614c2e46
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_model_finder.cpp
View file

@ -773,7 +773,12 @@ namespace smt {
for (auto const& kv : elems) { for (auto const& kv : elems) {
expr* t = kv.m_key; expr* t = kv.m_key;
expr* t_val = eval(t, true); expr* t_val = eval(t, true);
if (t_val && !already_found.contains(t_val)) { bool found = false;
if (t_val && !m.is_unique_value(t_val))
for (expr* v : values)
found |= m.are_equal(v, t_val);
if (t_val && !found && !already_found.contains(t_val)) {
values.push_back(t_val); values.push_back(t_val);
already_found.insert(t_val); already_found.insert(t_val);
} }
@ -875,9 +880,9 @@ namespace smt {
if (else_val) if (else_val)
pi->set_else(else_val); pi->set_else(else_val);
} }
for (expr* v : values) { for (expr* v : values)
pi->insert_new_entry(&v, v); pi->insert_new_entry(&v, v);
}
n->set_proj(p); n->set_proj(p);
TRACE("model_finder", n->display(tout << p->get_name() << "\n", m);); TRACE("model_finder", n->display(tout << p->get_name() << "\n", m););
} }