From b571e43f85f29fc55c9b3a98e8aed9c9ac49eec0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Apr 2020 13:28:46 -0700
Subject: [PATCH] fix #4146

---
 src/math/polynomial/polynomial.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 78ec0ec8b..c6e551a3c 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -794,11 +794,15 @@ namespace polynomial {
         ~monomial_manager() {
             dec_ref(m_unit);
             CTRACE("polynomial", !m_monomials.empty(),
-                   tout << "monomials leaked\n";
+                   tout << "monomials leaked (can happen during cancelation)\n";
                    for (auto * m : m_monomials) {
                        m->display(tout << m->id() << " " << m->ref_count() << " ") << "\n";
                    });
-            SASSERT(m_monomials.empty());
+            for (monomial* m : m_monomials) {
+                unsigned obj_sz = monomial::get_obj_size(m->size());
+                m_allocator->deallocate(obj_sz, m);                
+            }
+            m_monomials.reset();
             if (m_own_allocator)
                 dealloc(m_allocator);
         }