mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

fix #3391

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 13:04:30 -07:00
parent 19cdf08818
commit daadc1dd8c
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/opt/maxlex.cpp
View file

@ -19,6 +19,7 @@ Author:
--*/ --*/
#include "ast/ast_pp.h"
#include "opt/opt_context.h" #include "opt/opt_context.h"
#include "opt/maxsmt.h" #include "opt/maxsmt.h"
#include "opt/maxlex.h" #include "opt/maxlex.h"
@ -75,14 +76,20 @@ namespace opt {
} }
void update_assignment(model_ref & mdl) { void update_assignment(model_ref & mdl) {
mdl->set_model_completion(true);
bool first_undef = true, second_undef = false; bool first_undef = true, second_undef = false;
for (auto & soft : m_soft) { for (auto & soft : m_soft) {
if (first_undef && soft.value != l_undef) { if (first_undef && soft.value != l_undef) {
continue; continue;
} }
if (first_undef) {
SASSERT(soft.value == l_undef);
soft.set_value(l_true);
assert_value(soft);
first_undef = false; first_undef = false;
if (soft.value != l_false) { }
lbool v = mdl->is_true(soft.s) ? l_true : l_undef;; else if (soft.value != l_false) {
lbool v = mdl->is_true(soft.s) ? l_true : l_undef;
if (v == l_undef) { if (v == l_undef) {
second_undef = true; second_undef = true;
} }