From daadc1dd8cd154608a5ee1d941e4134a2147bc21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Mar 2020 13:04:30 -0700 Subject: [PATCH] fix #3391 Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 0507b0994..b29c069ef 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -19,6 +19,7 @@ Author: --*/ +#include "ast/ast_pp.h" #include "opt/opt_context.h" #include "opt/maxsmt.h" #include "opt/maxlex.h" @@ -75,14 +76,20 @@ namespace opt { } void update_assignment(model_ref & mdl) { + mdl->set_model_completion(true); bool first_undef = true, second_undef = false; for (auto & soft : m_soft) { if (first_undef && soft.value != l_undef) { continue; } - first_undef = false; - if (soft.value != l_false) { - lbool v = mdl->is_true(soft.s) ? l_true : l_undef;; + if (first_undef) { + SASSERT(soft.value == l_undef); + soft.set_value(l_true); + assert_value(soft); + first_undef = false; + } + else if (soft.value != l_false) { + lbool v = mdl->is_true(soft.s) ? l_true : l_undef; if (v == l_undef) { second_undef = true; }