mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixed memory leaks

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-07 18:06:13 +00:00
parent 778dd997d3
commit da01f237fd
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/propagate_ineqs_tactic.cpp
View file

@ -115,6 +115,7 @@ struct propagate_ineqs_tactic::imp {
out << "< oo";
out << "\n";
}
nm.del(k);
}
a_var mk_var(expr * t) {
@ -234,6 +235,7 @@ struct propagate_ineqs_tactic::imp {
SASSERT(k == GE);
bp.assert_lower(x, c_prime, strict);
}
nm.del(c_prime);
return true;
}
@ -309,6 +311,8 @@ struct propagate_ineqs_tactic::imp {
m_new_goal->assert_expr(m_util.mk_le(p, m_util.mk_numeral(rational(u), m_util.is_int(p))));
}
}
nm.del(l);
nm.del(u);
}
bool is_x_minus_y_eq_0(expr * t, expr * & x, expr * & y) {