Setting distinct range for each symbolic variable

[karthiv]

If the program has a statement

int a = Debug.makeSymbolicInteger("sym_1"); int b = Debug.makeSymbolicInteger("sym_2");

Is it possible to set the range of a from 1 to 100 and range of b from 1 to 10?

I see that there is generic max int and min int setting in jpf file, but is it possible for each variable?

[yannicnoller]

I think, in principle, you could extend the implementation of the Debug.makeSymbolicInteger method to also take a constraint as an additional parameter. But as a simple workaround, you can use the Debug.assume() function to add these additional constraints. For example:

Debug.assume(b > 0 && b < 11);