mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix ast leak in asserted_formulas::propagate_values()

Browse source 
Fixes issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-11-27 20:09:17 +00:00
parent db2f973e3e
commit d175c99542
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

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