From 480e5e999b2079e0f0477ca299fe81b47b300972 Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber-Caissier
 <philipp.schlehuber-caissier@telecom-sudparis.eu>
Date: Sun, 5 Jan 2025 13:18:35 +0100
Subject: [PATCH] Fix slight error in aiger

The negation of global equivalences for outputs
contained a slight error when the output corresponded
to a negated gate.

* spot/twaalgos/aiger.cc: Fix
* tests/core/ltlsynt.test: Test
---
 spot/twaalgos/aiger.cc  |  5 ++++-
 tests/core/ltlsynt.test | 12 ++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index 95c758ede..8c29dfe41 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -2061,7 +2061,10 @@ namespace
                       assert(it2 != output_names_all.end());
                       unsigned outnum = it2 - output_names_all.begin();
                       unsigned outvar = circuit.output(outnum);
-                      circuit.set_output(i, outvar + neg_repr);
+                      assert(outvar != -1u);
+                      if (neg_repr)
+                        outvar = circuit.aig_not(outvar);
+                      circuit.set_output(i, outvar);
                     }
               }
           }
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index dd3e4152c..d8a4c2f44 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -1304,3 +1304,15 @@ f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5'
 ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2
 sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx
 diff outx exp
+
+# Additional test for global equivalences
+# Specifically if the output is set to the negation of another output
+
+ltlsynt -f "((G((p0)<->(!(p1))))&&(((F(a))||(G(b)))<->(G(F(p0)))))" \
+        --outs "p1, p0" \
+        --verify --aiger | tail -n 1 > out
+
+cat > expected <<EOF
+Circuit was verified
+EOF
+diff out expected