diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 3e7dc7ef8..1f44729c7 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -159,6 +159,10 @@ public: // a is the coefficient by which we divided the term to normalize it lar_term get_normalized_by_min_var(mpq& a) const { + if (m_coeffs.empty()) { + a = mpq(1, 1); + return *this; + } a = m_coeffs.begin()->m_value; if (a.is_one()) { return *this;