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 d89ecd292..6f54cd425 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1360,3 +1360,16 @@ REALIZABLE REALIZABLE EOF diff out expected + +# 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 <