mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #4235

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-07 10:50:56 -07:00
parent 6a61e8dd5b
commit 54f38d004b
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/opt/maxlex.cpp
View file

@ -52,7 +52,7 @@ namespace opt {
ast_manager& m; ast_manager& m;
maxsat_context& m_c; maxsat_context& m_c;
void update_assignment() { bool update_assignment() {
model_ref mdl; model_ref mdl;
s().get_model(mdl); s().get_model(mdl);
if (mdl) { if (mdl) {
@ -60,6 +60,7 @@ namespace opt {
m_c.model_updated(mdl.get()); m_c.model_updated(mdl.get());
update_assignment(mdl); update_assignment(mdl);
} }
return mdl.get() != nullptr;
} }
void assert_value(soft& soft) { void assert_value(soft& soft) {
@ -158,7 +159,8 @@ namespace opt {
lbool is_sat = s().check_sat(asms); lbool is_sat = s().check_sat(asms);
switch (is_sat) { switch (is_sat) {
case l_true: case l_true:
update_assignment(); if (!update_assignment())
return l_undef;
SASSERT(soft.value == l_true || m.limit().get_cancel_flag()); SASSERT(soft.value == l_true || m.limit().get_cancel_flag());
break; break;
case l_false: case l_false: