From df872ce6d917d711a2e972f44428151a6e58df0a Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Thu, 16 Mar 2017 16:54:32 +0100
Subject: [PATCH] ltsmin: placement new requires placement delete

This commit fixes a bug that (randomly) occurs when
calling destructor of kripkecube.

*  spot/ltsmin/spins_kripke.hxx: here.
---
 spot/ltsmin/spins_kripke.hxx | 1 +
 1 file changed, 1 insertion(+)

diff --git a/spot/ltsmin/spins_kripke.hxx b/spot/ltsmin/spins_kripke.hxx
index 2c0884fd8..5d3911aec 100644
--- a/spot/ltsmin/spins_kripke.hxx
+++ b/spot/ltsmin/spins_kripke.hxx
@@ -266,6 +266,7 @@ namespace spot
         delete inner_[i].compressed_;
         delete inner_[i].uncompressed_;
       }
+    ::operator delete(manager_);
     delete[] inner_;
   }