From 1119a8018aff2222f7b31030b663dd0eb0f2f29f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Jan 2015 18:48:02 -0800 Subject: [PATCH] fix(util/buffer): destructor was not being invoked at erase and erase_elem This bug was producing a weird memory leak in the definition package. The methods erase and erase_elem are not used very often. This is why this bug was never detected. --- src/util/buffer.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/buffer.h b/src/util/buffer.h index 6926612af..ec8972f46 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -151,7 +151,7 @@ public: lean_assert(idx < size()); for (unsigned i = idx+1; i < size(); i++) m_buffer[i-1] = m_buffer[i]; - m_pos--; + pop_back(); } void erase_elem(T const & elem) {