Counter variables are commonly used in many computer applications for different purposes. Here is a typical example where a variable is used to measures the progress of some activity of interest:
If the exact value of the progress variable or the entire range of its values is not really required for checking the property of interest, then the use of this variable can cause unnecessary (potentially infinite) state space expansion. In this case, the progress variable can be reduced to a Boolean variable:
This modification immediately cuts down the number of states that need to be explored for this piece of code from ((2*MAXINT)+1)2 to only two possibilities: the progress variable taking only the value of true or false. Such small modifications can lead to exponential improvements in memory and time for a model checker.