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

fix #2959

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-09 12:38:05 -08:00
parent 1ef83351cb
commit 1eb4459325
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_mbp.cpp
View file

@ -64,6 +64,9 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
expr_ref_vector vals(m); expr_ref_vector vals(m);
obj_map<expr, expr*> val2expr; obj_map<expr, expr*> val2expr;
app* alit = to_app(t); app* alit = to_app(t);
if (alit->get_num_args() == 2) {
return expr_ref(m.mk_eq(alit->get_arg(0), alit->get_arg(1)), m);
}
for (expr * e1 : *alit) { for (expr * e1 : *alit) {
expr *e2; expr *e2;
val = model(e1); val = model(e1);
@ -79,7 +82,7 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
expr* e1 = alit->get_arg(i); expr* e1 = alit->get_arg(i);
expr* e2 = alit->get_arg(j); expr* e2 = alit->get_arg(j);
val = m.mk_eq(e1, e2); val = m.mk_eq(e1, e2);
if (model.is_true(val)) if (!model.is_false(val))
return expr_ref(m.mk_eq(e1, e2), m); return expr_ref(m.mk_eq(e1, e2), m);
} }
} }