mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
retrieve model before push
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8279b406ab
commit
5d772c1eb1
|
@ -33,12 +33,13 @@ namespace opt {
|
|||
lbool is_sat = m_solver->check_sat(0, nullptr);
|
||||
if (is_sat == l_true) {
|
||||
{
|
||||
m_solver->get_model(m_model);
|
||||
solver::scoped_push _s(*m_solver.get());
|
||||
while (is_sat == l_true) {
|
||||
if (m.canceled()) {
|
||||
return l_undef;
|
||||
}
|
||||
m_solver->get_model(m_model);
|
||||
|
||||
m_solver->get_labels(m_labels);
|
||||
m_model->set_model_completion(true);
|
||||
IF_VERBOSE(1,
|
||||
|
@ -48,6 +49,7 @@ namespace opt {
|
|||
// TBD: we can also use local search to tune solution coordinate-wise.
|
||||
mk_dominates();
|
||||
is_sat = m_solver->check_sat(0, nullptr);
|
||||
if (is_sat == l_true) m_solver->get_model(m_model);
|
||||
}
|
||||
}
|
||||
if (is_sat == l_undef) {
|
||||
|
|
Loading…
Reference in a new issue