From 034e4f469ee5aeb9e538d5dc9a2a38a12cde3811 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 22 Jan 2015 18:43:23 +0000 Subject: [PATCH] Fixed memory leak --- src/api/api_fpa.cpp | 5 ++++- src/util/mpf.h | 6 ++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 96c3e2eb6..d9f534499 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -696,6 +696,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpa_util().fm(); + unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); scoped_mpf val(mpfm); @@ -709,7 +710,9 @@ extern "C" { } unsigned sbits = val.get().get_sbits(); scoped_mpq q(mpqm); - mpqm.set(q, mpfm.sig_normalized(val)); + scoped_mpz sn(mpzm); + mpfm.sig_normalized(val, sn); + mpqm.set(q, sn); mpqm.div(q, mpfm.m_powers2(sbits - 1), q); std::stringstream ss; mpqm.display_decimal(ss, q, sbits); diff --git a/src/util/mpf.h b/src/util/mpf.h index 599e8e743..39eb7330e 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -146,14 +146,12 @@ public: bool sgn(mpf const & x) const { return x.sign; } const mpz & sig(mpf const & x) const { return x.significand; } - mpz sig_normalized(mpf const & x) { + void sig_normalized(mpf const & x, mpz & res) { mpf t; set(t, x); unpack(t, true); - mpz r; - mpz_manager().set(r, t.significand); + mpz_manager().set(res, t.significand); del(t); - return r; } const mpf_exp_t & exp(mpf const & x) const { return x.exponent; } mpf_exp_t exp_normalized(mpf const & x) {