schedule: assert that model-checker thread doesn't enter scheduler