mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #2929

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-03 08:36:37 -08:00
parent d418467089
commit 2398834206
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/qe/qe_mbp.cpp
View file

@ -67,12 +67,22 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
for (expr * e1 : *alit) {
expr *e2;
val = model(e1);
TRACE("qe", tout << mk_pp(e1, m) << " |-> " << val << "\n";);
if (val2expr.find(val, e2)) {
return expr_ref(m.mk_eq(e1, e2), m);
}
val2expr.insert(val, e1);
vals.push_back(val);
}
for (unsigned i = 0; i < alit->get_num_args(); ++i) {
for (unsigned j = i + 1; j < alit->get_num_args(); ++j) {
expr* e1 = alit->get_arg(i);
expr* e2 = alit->get_arg(j);
val = m.mk_eq(e1, e2);
if (model.is_true(val))
return expr_ref(m.mk_eq(e1, e2), m);
}
}
UNREACHABLE();
return expr_ref(nullptr, m);
}