From 927ea7046b17913340d4d41d24ed2d705b23954d Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Thu, 16 Apr 2020 22:08:07 +0200
Subject: [PATCH] unit_propagation: Correct a problem with multiple marks

* spot/twa/acc.cc: Don't create a conjunction of Inf with multiple marks
in unit_propagation.
---
 spot/twa/acc.cc | 30 ++++++++++++++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index 23dd7ef53..e7a47ecc7 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -2641,10 +2641,36 @@ namespace spot
       while (find_unit_clause(result, conj, fin, mark))
       {
         acc_code init_code;
+
         if (fin)
-          init_code = acc_code::fin(mark);
+        {
+          if (conj)
+          {
+            init_code = acc_code::t();
+            for (unsigned col : mark.sets())
+              init_code &= acc_code::fin({col});
+          } else
+          {
+            init_code = acc_code::f();
+            for (unsigned col : mark.sets())
+              init_code |= acc_code::fin({col});
+          }
+        }
         else
-          init_code = acc_code::inf(mark);
+        {
+          if (conj)
+          {
+            init_code = acc_code::t();
+            for (unsigned col : mark.sets())
+              init_code &= acc_code::inf({col});
+          }
+          else
+          {
+            init_code = acc_code::f();
+            for (unsigned col : mark.sets())
+              init_code |= acc_code::inf({col});
+          }
+        }
         if (conj)
           result = init_code & result.remove(mark, fin == conj);
         else