Light-Weight SMT-based Model Checking