diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index e3f035ae9..c08d0f901 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -204,11 +204,9 @@ namespace lp { print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl; ); mpq g = gcd_of_coeffs(ep.m_e); - if (g.is_zero()) { - if (ep.m_e.c().is_zero()) - return true; - return false; + SASSERT(ep.m_e.c().is_zero()); + return true; } if (g.is_one()) return true;