diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index cd32c011d..c0fb96a8b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -955,7 +955,7 @@ class theory_lra::imp { } else { init_left_side(st); - if (m_left_side.empty()) { + if (m_left_side.empty() && st.offset().is_zero()) { return get_zero(a.is_int(term)); } theory_var v = mk_var(term);