The verification always uses the continuous model checking and therefore increases the statespace size.
This is unnecessary in many (basic) situations.
Don't do that. Check the formula first and only do continuous checking if necessary.
Use Pointwise by default!!