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

check cancel flag to avoid unsound conflicts

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-19 11:43:52 -08:00
parent 32f8705ac3
commit 4350bd77ac
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/int_solver.cpp
View file

@ -208,6 +208,7 @@ namespace lp {
#endif
m_cut_vars.reset();
if (r == lia_move::undef) r = int_branch(*this)();
if (settings().get_cancel_flag()) r = lia_move::undef;
return r;
}
@ -854,7 +855,7 @@ namespace lp {
struct ex { explanation m_ex; lar_term m_term; mpq m_k; bool m_is_upper; };
vector<ex> cuts;
for (unsigned i = 0; i < num_cuts && has_inf_int() && !settings().get_cancel_flag(); ++i) {
for (unsigned i = 0; i < num_cuts && has_inf_int(); ++i) {
m_ex->clear();
m_t.clear();
m_k.reset();
@ -862,6 +863,8 @@ namespace lp {
if (r != lia_move::cut)
break;
cuts.push_back({ *m_ex, m_t, m_k, is_upper() });
if (settings().get_cancel_flag())
return lia_move::undef;
}
m_cut_vars.reset();
@ -882,7 +885,7 @@ namespace lp {
auto _check_feasible = [&](void) {
auto st = lra.find_feasible_solution();
if (!lra.is_feasible()) {
if (!lra.is_feasible() && !settings().get_cancel_flag()) {
lra.get_infeasibility_explanation(*m_ex);
return false;
}
@ -910,6 +913,9 @@ namespace lp {
bool feas = _check_feasible();
lra.pop(1);
if (settings().get_cancel_flag())
return lia_move::undef;
if (!feas)
return lia_move::conflict;

2
src/math/lp/nla_core.cpp
View file

@ -1567,6 +1567,8 @@ lbool core::check() {
{1, check3} };
check_weighted(3, checks);
if (lp_settings().get_cancel_flag())
return l_undef;
if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)
return l_false;
}