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

fix leak in asserted_formulas::propagate_values() for proof generation mode

Browse source 
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-11-29 10:49:52 +00:00
parent d175c99542
commit 5d289a8da5
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

@ -607,7 +607,7 @@ void asserted_formulas::propagate_values() {
unsigned sz = m_asserted_formulas.size(); unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
expr_ref n(m_asserted_formulas.get(i), m_manager); expr_ref n(m_asserted_formulas.get(i), m_manager);
proof * pr = m_asserted_formula_prs.get(i, 0); proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager);
TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";); TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
if (m_manager.is_eq(n)) { if (m_manager.is_eq(n)) {
expr * lhs = to_app(n)->get_arg(0); expr * lhs = to_app(n)->get_arg(0);