Data-based synthesis may indicate incorrect size of controlled system

When performing data-based synthesis on 'Initial Model/Tunnel.cif' at https://github.com/LMoormann/Eerste-Heinenoordtunnel with options --stats=ctrl-sys-states, a synthesis result is given with Controlled system: at most 1 state.

However, when exploring the untimed state space of the synthesized supervisor, the following output is given:

Found 1 state, 1 state to process.
Found 348,953 states, 347,953 states to process.
Found 648,060 states, 646,060 states to process.
...

Hence at most 1 state is incorrect. Most likely this is caused by BDD#satCount giving incorrect results. But this should be investigated.