From 1183a935c701e4bff3ebfa2150a11d1959b267ed Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Thu, 7 Jun 2018 15:11:16 +0200
Subject: [PATCH] fix a bug in aiger printer

* spot/twaalgos/aiger.cc: here
* tests/core/ltlsynt.test: add a non-regression test
---
 spot/twaalgos/aiger.cc  |  2 +-
 tests/core/ltlsynt.test | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index 8cf2f1c82..459e82c97 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -319,7 +319,7 @@ namespace spot
           int bddvar = aut->get_dict()->has_registered_proposition(ap, aut);
           assert(bddvar >= 0);
           bdd b = bdd_ithvar(bddvar);
-          if (bdd_implies(b, all_outputs)) // ap is an output AP
+          if (bdd_implies(all_outputs, b)) // ap is an output AP
             {
               bddvar_to_outputnum[bddvar] = output_names.size();
               output_names.emplace_back(ap.ap_name());
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 0b9d329df..8efc4948c 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -73,6 +73,34 @@ EOF
 ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --aiger > out
 diff out exp
 
+cat >exp <<EOF
+REALIZABLE
+aag 16 1 2 2 13
+2
+4 29
+6 33
+31
+31
+8 5 7
+10 3 8
+12 2 8
+14 4 7
+16 3 14
+18 2 14
+20 5 6
+22 2 20
+24 3 20
+26 17 25
+28 11 26
+30 19 23
+32 13 30
+i0 a
+o0 b
+o1 c
+EOF
+ltlsynt --ins='a' --outs='b,c' -f 'GFa <-> (GFb & GFc)' --aiger > out
+diff out exp
+
 cat >exp <<EOF
 translating formula done
 split inputs and outputs done