mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fixed memory leaks

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-20 17:57:00 -04:00
parent 47e95f8676
commit b03dc0af3b
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/parsers/smt/smtparser.cpp
View file

@ -1573,7 +1573,8 @@ private:
return false;
}
}
expr * p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
expr_ref p(m_manager);
p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
set_error("invalid pattern", children[0]);
return false;
@ -1581,8 +1582,11 @@ private:
patterns.push_back(p);
}
else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) {
app * sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
expr * p = m_manager.mk_pattern(1, &sk_hack);
app_ref sk_hack(m_manager);
sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
app * sk_hackp = sk_hack.get();
expr_ref p(m_manager);
p = m_manager.mk_pattern(1, &sk_hackp);
if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
set_error("invalid pattern", children[0]);
return false;