mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix overflow bug exposed by #2476

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-29 22:33:25 -03:00
parent a8bfab3273
commit de43e05102
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_pb.cpp
View file

@ -1597,6 +1597,9 @@ namespace smt {
value += coeff; value += coeff;
} }
} }
if (value >= 0) {
display_resolved_lemma(verbose_stream() << "not validated\n");
}
// std::cout << "bound: " << m_bound << " value " << value << " coeffs: " << m_active_vars.size() << " lemma is " << (value >= 0 ? "sat" : "unsat") << "\n"; // std::cout << "bound: " << m_bound << " value " << value << " coeffs: " << m_active_vars.size() << " lemma is " << (value >= 0 ? "sat" : "unsat") << "\n";
return value < 0; return value < 0;
} }
@ -1804,8 +1807,8 @@ namespace smt {
} }
if (g >= 2) { if (g >= 2) {
normalize_active_coeffs(); normalize_active_coeffs();
for (unsigned i = 0; i < m_active_vars.size(); ++i) { for (auto v : m_active_vars) {
m_coeffs[m_active_vars[i]] /= g; m_coeffs[v] /= static_cast<int>(g);
} }
m_bound = (m_bound + g - 1) / g; m_bound = (m_bound + g - 1) / g;
TRACE("pb", display_resolved_lemma(tout << "cut\n");); TRACE("pb", display_resolved_lemma(tout << "cut\n"););