mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
fix #4232
This commit is contained in:
parent
aa3749f678
commit
fc6bdb9708
|
@ -39,7 +39,8 @@ namespace opt {
|
||||||
if (!m.inc()) {
|
if (!m.inc()) {
|
||||||
return l_undef;
|
return l_undef;
|
||||||
}
|
}
|
||||||
|
if (!m_model)
|
||||||
|
return l_undef;
|
||||||
m_solver->get_labels(m_labels);
|
m_solver->get_labels(m_labels);
|
||||||
m_model->set_model_completion(true);
|
m_model->set_model_completion(true);
|
||||||
IF_VERBOSE(1,
|
IF_VERBOSE(1,
|
||||||
|
|
Loading…
Reference in a new issue