mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4105

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-26 22:59:19 -07:00
parent f1193986c9
commit 5434f3e31d
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/polynomial/polynomial.cpp
View file

@ -2653,6 +2653,9 @@ namespace polynomial {
m_tmp_linear_ms.push_back(mk_unit()); 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()); 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_as.reset();
m_tmp_linear_ms.reset(); m_tmp_linear_ms.reset();
return p; return p;

2
src/util/mpz.cpp
View file

@ -122,9 +122,11 @@ uint64_t u64_gcd(uint64_t u, uint64_t v) {
} }
template<bool SYNCH> template<bool SYNCH>
mpz_manager<SYNCH>::mpz_manager(): mpz_manager<SYNCH>::mpz_manager():
m_allocator("mpz_manager") { m_allocator("mpz_manager") {
#ifndef _MP_GMP #ifndef _MP_GMP
if (sizeof(digit_t) == sizeof(uint64_t)) { if (sizeof(digit_t) == sizeof(uint64_t)) {
// 64-bit machine // 64-bit machine