WARNING: state f25 is unreachable
WARNING: state f2 is unreachable
WARNING: state f27 is unreachable
WARNING: state f29 is unreachable
==> NOT SURE whether or not main.fstb terminates.