mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-29 08:49:51 +00:00
Code Activity

remove extraction of linear cores because it examines a stale core instead of the current core. A reintroduction of this feature would have to extract the lemma before the next solver call and save it aside in case the solver call returns l_undef

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-25 19:24:57 -08:00
parent 151be6ac9a
commit 5438d5ad89
1 changed files with 4 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/nla_stellensatz.cpp
View file

@ -115,18 +115,16 @@ namespace nla {
if (num_conflicts >= m_config.max_conflicts)
return l_undef;
while (backtrack(m_core)) {
++c().lp_settings().stats().m_stellensatz.m_num_backtracks;
++c().lp_settings().stats().m_stellensatz.m_num_backtracks;
lbool rb = m_solver.solve(m_core);
if (rb == l_false)
continue;
if (rb == l_undef) {
if (core_is_linear(m_core))
break;
return rb;
}
if (rb == l_undef)
return rb;
m_solver.update_values(m_values);
goto start_saturate;
}
++c().lp_settings().stats().m_stellensatz.m_num_conflicts;
conflict(m_core);
}
if (r == l_true && !set_model())
@ -1336,7 +1334,6 @@ namespace nla {
core.reset();
for (auto p : m_ex)
core.push_back(m_internal2external_constraints[p.ci()]);
return l_false;
}
return r;
}