mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
avoid crash on box models under cancellation. Issue # SASSERT(!m_box_models.empty());
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8aee7129f6
commit
0fdf01e410
|
@ -189,9 +189,10 @@ public:
|
|||
trace_bounds(m_trace_id.c_str());
|
||||
}
|
||||
|
||||
#define RUNDEF() { std::cout << __LINE__ << "\n"; return l_undef; }
|
||||
lbool mus_solver() {
|
||||
lbool is_sat = l_true;
|
||||
if (!init()) return l_undef;
|
||||
if (!init()) RUNDEF();
|
||||
init_local();
|
||||
trace();
|
||||
while (m_lower < m_upper) {
|
||||
|
@ -203,7 +204,7 @@ public:
|
|||
);
|
||||
is_sat = check_sat_hill_climb(m_asms);
|
||||
if (m.canceled()) {
|
||||
return l_undef;
|
||||
RUNDEF();
|
||||
}
|
||||
switch (is_sat) {
|
||||
case l_true:
|
||||
|
@ -219,7 +220,7 @@ public:
|
|||
}
|
||||
break;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
RUNDEF();
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
@ -229,14 +230,14 @@ public:
|
|||
}
|
||||
|
||||
lbool primal_dual_solver() {
|
||||
if (!init()) return l_undef;
|
||||
if (!init()) RUNDEF();
|
||||
init_local();
|
||||
trace();
|
||||
exprs cs;
|
||||
while (m_lower < m_upper) {
|
||||
lbool is_sat = check_sat_hill_climb(m_asms);
|
||||
if (m.canceled()) {
|
||||
return l_undef;
|
||||
RUNDEF();
|
||||
}
|
||||
switch (is_sat) {
|
||||
case l_true:
|
||||
|
@ -259,7 +260,7 @@ public:
|
|||
}
|
||||
break;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
RUNDEF();
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
@ -339,7 +340,7 @@ public:
|
|||
case s_primal_dual:
|
||||
return primal_dual_solver();
|
||||
}
|
||||
return l_undef;
|
||||
RUNDEF();
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics& st) const {
|
||||
|
|
|
@ -366,12 +366,16 @@ namespace opt {
|
|||
}
|
||||
|
||||
lbool context::execute_box() {
|
||||
if (m_box_index < m_objectives.size()) {
|
||||
SASSERT(m_box_index < m_box_models.size());
|
||||
if (m_box_index < m_box_models.size()) {
|
||||
m_model = m_box_models[m_box_index];
|
||||
++m_box_index;
|
||||
return l_true;
|
||||
}
|
||||
if (m_box_index < m_objectives.size()) {
|
||||
m_model = 0;
|
||||
++m_box_index;
|
||||
return l_undef;
|
||||
}
|
||||
if (m_box_index != UINT_MAX && m_box_index >= m_objectives.size()) {
|
||||
m_box_index = UINT_MAX;
|
||||
return l_false;
|
||||
|
@ -384,17 +388,14 @@ namespace opt {
|
|||
if (obj.m_type == O_MAXSMT) {
|
||||
solver::scoped_push _sp(get_solver());
|
||||
r = execute(obj, false, false);
|
||||
if (r == l_true) {
|
||||
m_box_models.push_back(m_model.get());
|
||||
}
|
||||
m_box_models.push_back(m_model.get());
|
||||
}
|
||||
else {
|
||||
m_box_models.push_back(m_optsmt.get_model(j));
|
||||
++j;
|
||||
}
|
||||
}
|
||||
if (r == l_true && m_objectives.size() > 0) {
|
||||
SASSERT(!m_box_models.empty());
|
||||
if (r == l_true && m_box_models.size() > 0) {
|
||||
m_model = m_box_models[0];
|
||||
}
|
||||
return r;
|
||||
|
@ -498,6 +499,9 @@ namespace opt {
|
|||
}
|
||||
|
||||
std::string context::reason_unknown() const {
|
||||
if (m.canceled()) {
|
||||
return Z3_CANCELED_MSG;
|
||||
}
|
||||
if (m_solver.get()) {
|
||||
return m_solver->reason_unknown();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue