From fedc6d475489f73eaa3317a6344d5e5ae03d61bf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 12:54:36 +0000 Subject: [PATCH] Fixed memory leak in fpa2bv tactic. --- src/tactic/fpa/fpa2bv_tactic.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index cfedb66d7..aa9277e39 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -93,9 +93,9 @@ class fpa2bv_tactic : public tactic { expr * sgn, *sig, *exp; expr_ref top_exp(m); m_conv.split_fp(new_curr, sgn, exp, sig); - m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)); - m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))); - m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))); + result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1))); + result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)))); + result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)))); } } } @@ -155,7 +155,7 @@ public: virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); }