From 5434f3e31df037f930ca1aa6b44f568d3a6df7ce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 22:59:19 -0700
Subject: [PATCH] fix #4105

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polynomial/polynomial.cpp | 3 +++
 src/util/mpz.cpp                   | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 7f4d26c8d..78ec0ec8b 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -2653,6 +2653,9 @@ namespace polynomial {
                 m_tmp_linear_ms.push_back(mk_unit());
             }
             polynomial * p = mk_polynomial(m_tmp_linear_as.size(), m_tmp_linear_as.c_ptr(), m_tmp_linear_ms.c_ptr());
+            for (auto& a : m_tmp_linear_as) {
+                m_manager.del(a);
+            }
             m_tmp_linear_as.reset();
             m_tmp_linear_ms.reset();
             return p;
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index a6b05a877..eb6754654 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -122,9 +122,11 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) {
 }
 
 
+
 template<bool SYNCH>
 mpz_manager<SYNCH>::mpz_manager():
     m_allocator("mpz_manager") {
+
 #ifndef _MP_GMP
     if (sizeof(digit_t) == sizeof(uint64_t)) {
         // 64-bit machine