mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Fixed memory leak in goal::update.

Browse source 
Fixes #567
This commit is contained in:
Christoph M. Wintersteiger 2016-04-18 17:18:16 +01:00
parent 6db0a15d29
commit 5d0db6d256
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/goal.cpp
View file

@ -145,13 +145,14 @@ void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
} }
typedef std::pair<expr *, bool> expr_pol; typedef std::pair<expr *, bool> expr_pol;
sbuffer<expr_pol, 64> todo; sbuffer<expr_pol, 64> todo;
expr_ref_vector tmp_exprs(m());
todo.push_back(expr_pol(f, true)); todo.push_back(expr_pol(f, true));
while (!todo.empty()) { while (!todo.empty()) {
if (m_inconsistent) if (m_inconsistent)
return; return;
expr_pol p = todo.back(); expr_pol p = todo.back();
expr * curr = p.first; expr * curr = p.first;
bool pol = p.second; bool pol = p.second;
todo.pop_back(); todo.pop_back();
if (pol && m().is_and(curr)) { if (pol && m().is_and(curr)) {
app * t = to_app(curr); app * t = to_app(curr);
@ -173,10 +174,12 @@ void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
} }
else { else {
if (!pol) if (!pol) {
curr = m().mk_not(curr); curr = m().mk_not(curr);
tmp_exprs.push_back(curr);
}
if (save_first) { if (save_first) {
f = curr; f = curr;
save_first = false; save_first = false;
} }
else { else {