Oh no, you have just proved formal verification useless! Or, if you have an outer event loop that should potentially run forever, you mark only that one loop accordingly (details depend on the system).