From ef39c4b533cc97f1e5cf58e31a16ef6a1a9d6d13 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 31 Dec 2019 12:44:38 -0800
Subject: [PATCH] ignore term's zero coefficients in add_monomial()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lar_term.h | 2 ++
 1 file changed, 2 insertions(+)

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);