From 9411dab7387bec6bb0044bfde8b0b6366271ca76 Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Tue, 9 Jun 2020 17:04:26 +0200
Subject: [PATCH] lpar13: avoid leak when counterexample detected

* spot/mc/lpar13.hh: Here.
---
 spot/mc/lpar13.hh | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/spot/mc/lpar13.hh b/spot/mc/lpar13.hh
index d8ee87005..272b1820b 100644
--- a/spot/mc/lpar13.hh
+++ b/spot/mc/lpar13.hh
@@ -95,6 +95,11 @@ namespace spot
     virtual ~lpar13()
     {
       map.clear();
+      while (!todo.empty())
+        {
+          sys_.recycle(todo.back().it_kripke, tid_);
+          todo.pop_back();
+        }
     }
 
     bool run()
@@ -353,14 +358,19 @@ namespace spot
                           while (!bfs.empty())
                             {
                               auto* e = bfs.front();
+                              sys_.recycle(e->it_kripke, tid_);
                               bfs.pop();
                               delete e;
                             }
+                          sys_.recycle(front->it_kripke, tid_);
+                          delete front;
 
                           // update acceptance
                           acc |= mark;
                           if (twa_->acc().accepting(acc))
-                            return res;
+                            {
+                              return res;
+                            }
 
                           const product_state* q = &(it->first);
                           ctrx_element* root = new ctrx_element({
@@ -386,6 +396,8 @@ namespace spot
               front->it_prop->reset();
               front->it_kripke->next();
             }
+          sys_.recycle(front->it_kripke, tid_);
+          delete front;
         }
 
       // never reach here;