From 65bc67f300ecaa07fa027dfada96c026b34d9945 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 25 Oct 2022 11:53:05 +0200
Subject: [PATCH] relabel_here: make sure free_bddpair is called

* spot/twaalgos/relabel.cc (relabel_here): This function has multiple
exit paths, and none of them were calling bdd_freepair.  Use a
unique_ptr to ensure that.
---
 spot/twaalgos/relabel.cc | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc
index 22eddd893..ac1556aec 100644
--- a/spot/twaalgos/relabel.cc
+++ b/spot/twaalgos/relabel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et
+// Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -26,7 +26,7 @@ namespace spot
   void
   relabel_here(twa_graph_ptr& aut, relabeling_map* relmap)
   {
-    bddPair* pairs = bdd_newpair();
+    std::unique_ptr<bddPair> pairs(bdd_newpair());
     auto d = aut->get_dict();
     std::vector<int> vars;
     std::set<int> newvars;
@@ -53,7 +53,7 @@ namespace spot
           {
             int newv = aut->register_ap(p.second);
             newvars.insert(newv);
-            bdd_setpair(pairs, oldv, newv);
+            bdd_setpair(pairs.get(), oldv, newv);
           }
         else
           {
@@ -64,7 +64,7 @@ namespace spot
                                 return false;
                               });
             bdd newb = formula_to_bdd(p.second, d, aut);
-            bdd_setbddpair(pairs, oldv, newb);
+            bdd_setbddpair(pairs.get(), oldv, newb);
             bool_subst = true;
           }
       }
@@ -75,7 +75,7 @@ namespace spot
       static_cast<op_t>(bdd_veccompose) : static_cast<op_t>(bdd_replace);
     for (auto& t: aut->edges())
       {
-        bdd c = (*op)(t.cond, pairs);
+        bdd c = (*op)(t.cond, pairs.get());
         t.cond = c;
         if (c == bddfalse)
           need_cleanup = true;