Fix loop assign clause for Kani

[thanhnguyen-aws]

This PR fixes the bug that Kani only take the first target of the whole assign clause for loop.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

As commented out-of-band: I believe the fix should instead be made in Kani so that it produces an irept that has a single sub which in turn hold the irept with all the assigns clauses (i.e., in that inner irept each assigns clause will be one of the sub elements).

[thanhnguyen-aws]

As commented out-of-band: I believe the fix should instead be made in Kani so that it produces an irept that has a single sub which in turn hold the irept with all the assigns clauses (i.e., in that inner irept each assigns clause will be one of the sub elements).

As commented out-of-band: I believe the fix should instead be made in Kani so that it produces an irept that has a single sub which in turn hold the irept with all the assigns clauses (i.e., in that inner irept each assigns clause will be one of the sub elements).

Thanks, let me try from Kani side.