From ebfb2a4a1e1c52da405673791ef5f0eea95d38e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 May 2018 18:27:45 -0700 Subject: [PATCH] Fix mbp to respect reduce_all_selects option Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 1390c0ae5..438f1c061 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -592,10 +592,11 @@ public: flatten_and(fml); - do_qe_lite(vars, fml); while (!vars.empty()) { + do_qe_lite(vars, fml); + do_qe_bool(mdl, vars, fml); // sort out vars into bools, arith (int/real), and arrays @@ -613,21 +614,19 @@ public: vars.reset (); // project arrays - if (!array_vars.empty()) { - qe::array_project_plugin ap(m); - ap(mdl, array_vars, fml, vars, m_reduce_all_selects); - SASSERT (array_vars.empty ()); - m_rw (fml); - SASSERT (!m.is_false (fml)); - } - + qe::array_project_plugin ap(m); + ap(mdl, array_vars, fml, vars, m_reduce_all_selects); + SASSERT (array_vars.empty ()); + m_rw (fml); + SASSERT (!m.is_false (fml)); + TRACE ("qe", tout << "extended model:\n"; model_pp (tout, mdl); tout << "Vars: " << vars << "\n"; ); - } + // project reals, ints and other variables. if (!other_vars.empty ()) { TRACE ("qe", tout << "Other vars: " << other_vars << "\n";