test for issue #3653

[kroening]

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• n/a My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 3791557).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96399703

[tautschnig]

Please provide sufficient information in here (and in the commit message!) so that one doesn't have to go through extra hoops to figure out what this is about. Moreover, this isn't the same code as in the bug report and it's not clear whether both assertions in this test now fail or just one of them.

[NlightNFotis]

HI @kroening, would it be possible to address @tautschnig 's comment so that we can get this merged? Also it will need a rebase on develop, as CI has had an extensive rework since then.

[NlightNFotis]

Going ahead and closing this on the following basis:

1. Last response on this issue was 1 year ago, rendering this PR inactive,
2. A PR (Support non-heap allocated flexible arrays #6661) has been merged with a fix for the issue this PR links to, along with a test that appears to be based on the test added in this PR.
3. The issue this PR references has subsequently been closed.

If you believe this has been in err, feel free to reopen the issue.