mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Fixed memory leak in fpa2bv tactic.
This commit is contained in:
parent
f54c430756
commit
fedc6d4754
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue