Due to the glitch in the liveness track (see the update on the
results) it seems
to be time to enforce witnesses next year, at least in a mild form.
strict rule would be the same as in the SAT competition. If no
witness is provided
for a satisfiable instance, the instance is not scored. A wrong
mark the model checker as buggy and it will not take part in the
Is this too strict?