From 3712cbdbfd61237779219c49d06fb69e4d77f852 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Feb 2023 13:33:40 -0800 Subject: [PATCH] fix #6559 Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index f4ebce594ad..12365b2040e 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1513,10 +1513,11 @@ namespace qe { propagate_assignment(*model_eval); VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); SASSERT(m_current->fml()); - if (l_true != m_solver.check()) { - return l_true; - } + if (l_true != m_solver.check()) + return l_true; m_solver.get_model(model); + if (!model) + return l_undef; model_eval = alloc(model_evaluator, *model); search_tree* st = m_current; update_current(*model_eval, false);