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

fix mem leak in quantifier_info::insert_qinfo on timeout

Browse source
This commit is contained in:
Nuno Lopes 2016-04-19 02:17:12 -07:00
parent b512212d41
commit 417c80edbc
2 changed files with 4 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_model_finder.cpp
View file

@ -1756,16 +1756,16 @@ namespace smt {
void insert_qinfo(qinfo * qi) { void insert_qinfo(qinfo * qi) {
// I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal. // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal.
scoped_ptr<qinfo> q(qi);
ptr_vector<qinfo>::iterator it = m_qinfo_vect.begin(); ptr_vector<qinfo>::iterator it = m_qinfo_vect.begin();
ptr_vector<qinfo>::iterator end = m_qinfo_vect.end(); ptr_vector<qinfo>::iterator end = m_qinfo_vect.end();
for (; it != end; ++it) { for (; it != end; ++it) {
checkpoint(); checkpoint();
if (qi->is_equal(*it)) { if (qi->is_equal(*it)) {
dealloc(qi);
return; return;
} }
} }
m_qinfo_vect.push_back(qi); m_qinfo_vect.push_back(q.detach());
TRACE("model_finder", tout << "new quantifier qinfo: "; qi->display(tout); tout << "\n";); TRACE("model_finder", tout << "new quantifier qinfo: "; qi->display(tout); tout << "\n";);
} }

8
src/util/util.h
View file

@ -226,9 +226,7 @@ public:
} }
~scoped_ptr() { ~scoped_ptr() {
if (m_ptr) { dealloc(m_ptr);
dealloc(m_ptr);
}
} }
T * operator->() const { T * operator->() const {
@ -253,9 +251,7 @@ public:
scoped_ptr & operator=(T * n) { scoped_ptr & operator=(T * n) {
if (m_ptr != n) { if (m_ptr != n) {
if (m_ptr) { dealloc(m_ptr);
dealloc(m_ptr);
}
m_ptr = n; m_ptr = n;
} }
return *this; return *this;