mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix bound miss-computation, include sporadic nra check for #4913

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-24 03:22:43 -08:00
parent 8546cf97d7
commit 21c626e3ee
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1470,7 +1470,7 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
if (n < checks[i].first) {
seen.insert(i);
checks[i].second();
bound -= n;
bound -= checks[i].first;
break;
}
n -= checks[i].first;
@ -1523,9 +1523,14 @@ lbool core::check(vector<lemma>& l_vec) {
{ 2, check2 },
{ 1, check3 }};
check_weighted(3, checks);
if (!conflict_found() && m_nla_settings.run_nra() && random() % 30 == 0) {
ret = m_nra.check();
m_stats.m_nra_calls++;
}
}
if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) {
ret = m_nra.check();
m_stats.m_nra_calls++;
}