From 603597a22ebdfc90a1cdddf5ed0f41ef89bc00a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Dec 2022 12:40:39 -0800 Subject: [PATCH] deal with cancellation in qe for #6500 Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index d859880d8..f4ebce594 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1437,13 +1437,12 @@ namespace qe { res = m_solver.check(); if (res == l_true && has_uninterpreted(m, m_fml)) res = l_undef; - if (res == l_true) { + if (res == l_true) + res = final_check(); + if (res == l_true) is_sat = true; - final_check(); - } - else { + else break; - } } if (res == l_undef) { free_vars.append(num_vars, vars); @@ -1501,30 +1500,33 @@ namespace qe { private: - void final_check() { - model_ref model; + lbool final_check() { + model_ref model; m_solver.get_model(model); + if (!model) + return l_undef; scoped_ptr model_eval = alloc(model_evaluator, *model); - while (true) { + while (m.inc()) { TRACE("qe", model_v2_pp(tout, *model);); - while (can_propagate_assignment(*model_eval)) { + while (can_propagate_assignment(*model_eval)) propagate_assignment(*model_eval); - } VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); SASSERT(m_current->fml()); if (l_true != m_solver.check()) { - return; + return l_true; } m_solver.get_model(model); model_eval = alloc(model_evaluator, *model); search_tree* st = m_current; update_current(*model_eval, false); - if (st == m_current) { + if (st == m_current) break; - } - } - pop(*model_eval); + } + if (!m.inc()) + return l_undef; + pop(*model_eval); + return l_true; } ast_manager& get_manager() override { return m; }