Remove unneeded unwinds from unbounded benchmarks

[qinheping]

Description of changes:

There are unreachable loops in the code snippet compiled from generator resume. For example, in the goto program compiled from the benchmark moved_locals.rs:

     8: ASSERT false // KANI_CHECK_ID_moved_locals.c1d95029::moved_locals_3
        // 716 file /Users/qinhh/Repos/kani/qinheping/tests/kani/Generator/rustc-generator-tests/moved-locals.rs line 71 column 5 function overlap_x_and_y::{closure#0}
        ASSERT 0 ≠ 0 // [KANI_CHECK_ID_moved_locals.c1d95029::moved_locals_3] generator resumed after completion
        // 717 file /Users/qinhh/Repos/kani/qinheping/tests/kani/Generator/rustc-generator-tests/moved-locals.rs line 71 column 5 function overlap_x_and_y::{closure#0}
        ASSUME 0 ≠ 0
        // 718 file /Users/qinhh/Repos/kani/qinheping/tests/kani/Generator/rustc-generator-tests/moved-locals.rs line 71 column 5 function overlap_x_and_y::{closure#0}
        GOTO 8

The jump-back instruction GOTO 8 is unreachable as it is after ASSUME 0 ≠ 0.

However, such unreachable loops can actually be correctly handle by CBMC. So we can remove the unwinding numbers from the benchmarks modified in this PR.

Resolved issues:

Resolves #ISSUE-NUMBER

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

• How is this change tested?

• Is this a refactor change?

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

I'm curious why you decided to remove the unwind in these tests. Did you try other tests as well? I'm assuming we have a lot of unwind annotations that are not quite needed anymore.

[qinheping]

I'm curious why you decided to remove the unwind in these tests. Did you try other tests as well? I'm assuming we have a lot of unwind annotations that are not quite needed anymore.

I tried the synthesizer on all benchmarks with unwinding numbers and investigated what kind of loops are in the benchmarks. Some of those benchmarks are actually unbounded even though we specify unwinding number for them. So, to better track which benchmarks should be the target of the synthesizer, I decided to remove unwinding numbers from those unbounded benchmarks (assuming the input become unbounded).

Yes, there are more unbounded benchmarks in which we can remove the unwinding numbers. This PR now only covers loops caused by generators. Let me also add other kind of loops into this PR.