Add model checker check before trylock