To do #10434
Automatically detect the bound in HiFrog for the sake of completeness
Developing a preprocessing mechanism to detect the necessary depth of unrolling the program.(completeness threshold)
Then we can claim on verification of those instances, not just falsification.