Okay thanks! So what I don't get is, what's the point of bounding loops then? If it's already simulating the program up to 1M instructions and rejecting it if simulation doesn't prove termination (bounded model checking?), then can't it still do that when there's no loop bound?
Because I kind of expected the algorithm would say "hey this loop is bounded up to 4K, this nested one is up to 3K, therefore I can't prove the total is below 1M, therefore I reject", but from your description it sounds like it actually does some kind of bounded model checking up to 1M instructions instead of taking shortcuts like this? Or did you mean it actually does take shortcuts like this?
