I've had a quick look @ the model checking options. What I understand it does with the constants is:

- It makes them range according to the values set for MAXINT and MININT. So, to explore more states, just increase these values. Note: checking time is likely to grow exponentially.

- By default, these are enumerated orderly, starting at one. Since it stops when a problem is found, these are usually with a small value. If you want them to be explored in another order, you can check the box "Randomise enumeration of variables". But then, counterexamples won't use small values, which are often easier to deal with.

Best,