Support comparing arrays of non-constant size with array_equal

[tautschnig]

Using simple type equality is too strict for arrays of non-constant size: we introduce a fresh symbol for the size of each dynamically allocated object of non-constant size. Consequently, two dynamically allocated arrays of non-constant size will never pass type equality checking, even when their underlying sizes are the same.

We now explicitly compare the sizes of the two arrays passed to array_equal when types are not trivially equal.

Fixes: #8176

• 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).
• 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.

[kroening]

I am wondering what happens when you compare two arrays with element types that have different sizes?

[tautschnig]

I am wondering what happens when you compare two arrays with element types that have different sizes?

With the proposed patch the element sizes wouldn't actually matter anymore. Which, of course, raises the question: what is the semantics of array_equal that we want? What if one of the arguments isn't an array?

[peterschrammel]

Do you expect it to check type equality or content equality?