model: record the number of feasible executions