WARNING: state f0 is unreachable
WARNING: state f5 is unreachable
==> NOT SURE whether or not main.fstb terminates.