fix #4105

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 27, 2020 · 5434f3e · 5434f3e
1 parent f119398
commit 5434f3e
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git 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
@@ -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