mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

handle zero rows correctly

Browse source
This commit is contained in:
Lev Nachmanson 2024-08-27 08:59:33 -10:00
parent 178411ad0c
commit 1a99fa56cb
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -204,11 +204,9 @@ namespace lp {
print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl; print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl;
); );
mpq g = gcd_of_coeffs(ep.m_e); mpq g = gcd_of_coeffs(ep.m_e);
if (g.is_zero()) { if (g.is_zero()) {
if (ep.m_e.c().is_zero()) SASSERT(ep.m_e.c().is_zero());
return true; return true;
return false;
} }
if (g.is_one()) if (g.is_one())
return true; return true;