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 < (GFb & GFc)' --aiger > out +diff out exp + cat >exp <