From 5a441e1b9394d9c571b4c16b9807182183e43505 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 20 Jan 2017 14:41:00 +0100
Subject: [PATCH] fix some incorrect AP registrations

* spot/ltsmin/ltsmin.cc: Do not forget to register dead.
* spot/twa/twaproduct.cc: Use copy_ap_of() instead of
register_all_propositions_of() because the latter does
do update ap().
---
 NEWS                   | 8 +++++++-
 spot/ltsmin/ltsmin.cc  | 5 +++--
 spot/twa/twaproduct.cc | 9 ++++-----
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 7b5e052f7..bc00ef2d4 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,12 @@
 New in spot 2.3.0.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - spot::otf_product() was incorrectly registering atomic
+    propositions.
+
+  - spot::ltsmin_model::kripke() forgot to register the "dead"
+    proposition.
 
 New in spot 2.3 (2017-01-19)
 
diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc
index 32d76e547..fa245687c 100644
--- a/spot/ltsmin/ltsmin.cc
+++ b/spot/ltsmin/ltsmin.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE)
+// Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -1118,6 +1118,7 @@ namespace spot
     // twa::ap() works.
     for (auto ap: *to_observe)
       res->register_ap(ap);
+    res->register_ap(dead);
     return res;
   }
 
diff --git a/spot/twa/twaproduct.cc b/spot/twa/twaproduct.cc
index a124b43fa..2a7756135 100644
--- a/spot/twa/twaproduct.cc
+++ b/spot/twa/twaproduct.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -306,9 +306,8 @@ namespace spot
         left_kripke_ = false;
       }
 
-    auto d = get_dict();
-    d->register_all_propositions_of(&left_, this);
-    d->register_all_propositions_of(&right_, this);
+    copy_ap_of(left_);
+    copy_ap_of(right_);
 
     assert(num_sets() == 0);
     auto left_num = left->num_sets();