From 60929667024ecd5510f5ebee2f29403b7a0af409 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 May 2017 13:17:26 -0700
Subject: [PATCH] fix(library/parray): missing desctrutor/constructor
 invocations at reroot

---
 src/library/parray.h         |  3 ++-
 src/tests/library/parray.cpp | 43 +++++++++++++++++++++++++++++++++++-
 2 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/src/library/parray.h b/src/library/parray.h
index 5b0a11a405..acab136ee7 100644
--- a/src/library/parray.h
+++ b/src/library/parray.h
@@ -215,7 +215,7 @@ class parray {
                 if (sz == capacity(vs))
                     vs = expand(vs, sz);
                 c->m_idx  = sz;
-                vs[sz]    = p->elem();
+                new (vs + sz) T(p->elem());
                 sz++;
                 break;
             case PopBack:
@@ -225,6 +225,7 @@ class parray {
                 } else {
                     *c->m_elem = vs[sz];
                 }
+                (vs + sz)->~T();
                 c->m_kind = PushBack;
                 c->m_idx  = sz;
                 break;
diff --git a/src/tests/library/parray.cpp b/src/tests/library/parray.cpp
index 97c33df2d7..0d9a31d4ea 100644
--- a/src/tests/library/parray.cpp
+++ b/src/tests/library/parray.cpp
@@ -126,6 +126,47 @@ static void tst_perf(unsigned sz, unsigned n) {
     }
 }
 
+class Foo {
+    unsigned * m_data;
+public:
+    Foo():m_data(new unsigned(1)) {}
+    Foo(Foo const & src):m_data(new unsigned(*src.m_data)) {}
+    Foo(Foo && src):m_data(new unsigned(*src.m_data)) {}
+    Foo(unsigned n):m_data(new unsigned(n)) {}
+    ~Foo() { delete m_data; }
+
+    Foo & operator=(Foo const & src) {
+        *m_data = *src.m_data;
+        return *this;
+    }
+
+    Foo & operator=(Foo const && src) {
+        *m_data = *src.m_data;
+        return *this;
+    }
+
+    unsigned get_val() const { return *m_data; }
+};
+
+static void tst4() {
+    parray<Foo> v1;
+    v1.push_back(Foo(2));
+    v1.push_back(Foo(3));
+    parray<Foo> v2 = v1;
+    for (unsigned i = 0; i < 10; i++)
+        v1.push_back(Foo(i));
+    v1.set(0, Foo(100));
+    v1.set(1, Foo(100));
+    lean_assert(v2.size() == 2);
+    lean_assert(v2[0].get_val() == 2);
+    lean_assert(v2[1].get_val() == 3);
+    parray<Foo> v3 = v1;
+    v1.pop_back();
+    v1.pop_back();
+    lean_assert(v1.size() == 10);
+    lean_assert(v3.size() == 12);
+}
+
 int main() {
     save_stack_info();
     initialize_util_module();
@@ -139,7 +180,7 @@ int main() {
     tst1();
     tst2();
     tst3(100000);
-
+    tst4();
     tst_perf(100000, 10000);
 
     finalize_library_module();