Generalize input limits for validation

[ngsrinivas]

Commit 7ed85fc introduced a limit to the input range to prevent counterexamples that occur due to overflow of the 64-bit bitvector.

This is believed to be due to integer overflows that happen either in the source program or the sampled program, but not the other. We need to see an example to be concrete about this.

Should we replicate the overflow behaviors that happen in the source in the optimized programs, i.e., optimized(.) == source(.) even when there are overflows in the output within the source program? If not, how does one set the limit for the inputs to the source program while validating the optimized program?