LAR bug
Guillermo Alberto Perez reported a case where ltlsynt --algo=lar
builds an incorrect controller.
The bug can be reduced to the following situation where the to_parity()
function output a DPA that is not equivalent to its input.
The word a & b; cycle{a & !b; !a & b}
is accepted by the input automaton, but not by the output.
Reverting 516e9536 makes the problem disappear.