SAT: an example of Büchi automaton that is not a Büchi automaton...
The org documentation for SAT-based reduction shows the following example:
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)"
however the result is not displayed as a Büchi automaton (although it seems to be). There is probably a function that forgot to set the state-based property.