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