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

fix ubuntu's build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-10-07 13:54:03 -07:00 committed by Lev Nachmanson
parent ea50208ad6
commit 4bd815852d
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/dioph_eq.cpp
View file

@ -259,9 +259,10 @@ namespace lp {
Then sum((coeff_i/g)*x_i) <= floor(-new_c) or sum((coeff_i/g)*x_i) >= ceil(-new_c) Then sum((coeff_i/g)*x_i) <= floor(-new_c) or sum((coeff_i/g)*x_i) >= ceil(-new_c)
*/ */
if (lra.settings().stats().m_dio_conflicts % lra.settings().dio_cut_from_proof_period() == 0) { if (lra.settings().stats().m_dio_conflicts % lra.settings().dio_cut_from_proof_period() == 0) {
bool has_fresh = std::any_of(ep.m_e.begin(), ep.m_e.end(), [this](const auto& p) { bool has_fresh = false;
return is_fresh_var(p.j()); for (const auto& p : ep.m_e)
}); if (has_fresh = is_fresh_var(p.j()))
break;
if (!has_fresh) { // consider remove all fresh variables in a copy of m_e and report the conflict if (!has_fresh) { // consider remove all fresh variables in a copy of m_e and report the conflict
// prepare int_solver for reporting // prepare int_solver for reporting
lar_term& t = lia.get_term(); lar_term& t = lia.get_term();