From 487642686661670d7cd8ff201881355480255c3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Feb 2019 18:15:24 -0800 Subject: [PATCH] project Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbi.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 77f910260..30682d667 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -294,15 +294,15 @@ namespace qe { } /** - * \brief project non-arithmetical private symbols. + * \brief project private symbols. */ void euf_arith_mbi_plugin::project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) { term_graph tg(m); func_decl_ref_vector shared(m_shared); - for (app* a : avars) shared.push_back(a->get_decl()); + //for (app* a : avars) shared.push_back(a->get_decl()); tg.set_vars(shared, false); tg.add_lits(lits); - lits.reset(); + //lits.reset(); lits.append(tg.project(*mdl.get())); TRACE("qe", tout << "project: " << lits << "\n";); }