From 82311c3e3b7ddc9d74a5642e10bddf74cbd6966b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 17 Feb 2024 16:57:31 +0100
Subject: [PATCH] ltlsynt: fix the case where AP removal is disabled and decomp
 fails

* bin/ltlsynt.cc: Correctly update the output variables in the case
decomposition failed and AP removal is disabled.
* tests/core/ltlsynt.test: Add a test case.
---
 bin/ltlsynt.cc          | 6 ++++++
 tests/core/ltlsynt.test | 4 ++++
 2 files changed, 10 insertions(+)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 2b0facc57..d2957855f 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -467,6 +467,12 @@ namespace
                   sub_outs[0].insert(ap);
               }
           }
+        else
+          {
+            for (const std::string& apstr: output_aps)
+              sub_outs[0].insert(spot::formula::ap(apstr));
+          }
+
       }
     std::vector<std::vector<std::string>> sub_outs_str;
     std::transform(sub_outs.begin(), sub_outs.end(),
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 14a18b9c3..28b846abd 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -1143,3 +1143,7 @@ ltlsynt --ins='/^in/,/env/' --outs='/^out/,/control/' \
   -f 'G(controlenv <-> input)' 2>err && :
 test $? -eq 2
 grep 'controlenv.*matches both' err
+
+
+ltlsynt --polarity=1 --global-e=1 -f 'G(i -> Xo) & G(!i -> F!o)' --real
+ltlsynt --polarity=0 --global-e=0 -f 'G(i -> Xo) & G(!i -> F!o)' --real