SMT2 Incremental: support array-to-array typecasts

[tautschnig]

Add handling for typecast expressions between two array types in the incremental SMT2 decision procedure. This is needed for SIMD operations (e.g. regression/cbmc/SIMD1) where arrays are reinterpreted with different element sizes.

Changes:

• gather_dependent_expressions: detect typecast_exprt where both source and target types are array_typet, adding them as dependent expressions
• define_array_typecast_function: new method that creates an SMT array function for the target type and asserts element-by-element constraints using concatenation (widening) or extraction (narrowing)
• define_dependent_functions: add branch to call the new method
• convert_expr_to_smt.cpp: add UNHANDLED_CASE sentinel for array-to-array typecast (the expression is pre-substituted by the decision procedure)
• Unit test for the UNHANDLED_CASE and sort conversion
• Remove no-new-smt tag from SIMD1 regression test

Fixes: #8075

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