mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix #4234
This commit is contained in:
parent
da9b037f2a
commit
6a61e8dd5b
|
@ -305,7 +305,10 @@ namespace opt {
|
|||
s.get_model(m_model);
|
||||
s.get_labels(m_labels);
|
||||
model_updated(m_model.get());
|
||||
}
|
||||
if (!m_model) {
|
||||
is_sat = l_undef;
|
||||
}
|
||||
}
|
||||
if (is_sat != l_true) {
|
||||
TRACE("opt", tout << m_hard_constraints << " " << asms << "\n";);
|
||||
if (!asms.empty()) {
|
||||
|
|
Loading…
Reference in a new issue