From 1eb4459325f6b01dd2e28ec8cb8b39143554e409 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Feb 2020 12:38:05 -0800 Subject: [PATCH] fix #2959 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index d82b3f1bc..366d70075 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -64,6 +64,9 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) { expr_ref_vector vals(m); obj_map val2expr; 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) { expr *e2; 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* e2 = alit->get_arg(j); 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); } }