diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h
index d3cb3293a..7ce1e3f88 100644
--- a/src/util/lp/lar_term.h
+++ b/src/util/lp/lar_term.h
@@ -29,6 +29,8 @@ class lar_term {
 public:
     lar_term() {}
     void add_monomial(const mpq& c, unsigned j) {
+        if (c.is_zero())
+            return;
         auto *e = m_coeffs.find_core(j);        
         if (e == nullptr) {
             m_coeffs.insert(j, c);