From 2398834206b4b7ef4a9cf4dbc8bf4873110f3a14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 3 Feb 2020 08:36:37 -0800 Subject: [PATCH] fix #2929 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index becaeb049..d82b3f1bc 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -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); }