From 8d59355b8815a2e4ee4c76bf241494d3e6139533 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 14:37:51 -0700 Subject: [PATCH] fix #3750 Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_term.h | 4 ++++ 1 file changed, 4 insertions(+) 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;