Maybe I missing something? (like ltlsynt dualising the automaton, etc.)

Here is what I tried. Into file synthesis.cc, add:

#include "spot/parseaut/public.hh"

Then in line 822, comment out:

    // auto aut = trans.run(f);

and instead add:

    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
    auto parsed_aut = parse_aut("/tmp/spec.hoa", dict);
    if (parsed_aut->aborted)
      abort();
    auto aut = parsed_aut->aut;

This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula.
Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'):

./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no

and provide the correct --ins and --outs arguments, and any formula with one of those propositions.

The tool outputs expected implementations on toy examples,
but on a larger example attached it outputs "unrealizable" instead of "realizable".
That is why the question.