From 528bb507b287c23447866d10c102d39a61735174 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 7 Oct 2014 13:01:35 +0100
Subject: [PATCH] DoC: fix memory leak

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index e5a6fd97f..adc7e959a 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -82,6 +82,7 @@ void doc_manager::deallocate(doc* src) {
     if (!src) return;
     m.deallocate(&src->pos());
     src->neg().reset(m);
+    src->~doc();
     m_alloc.deallocate(sizeof(doc), src);
 }
 void doc_manager::copy(doc& dst, doc const& src)  {