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