The is_checked function should decide whether a state still has to be checked. This could be done in any way. Relevant cases are:
the state has been checked
(future work): it is decided via proof information that this state does not have to be checked
Verify that the counter for checked states is correct in either way.