Re-enable array theory as default for array size above threshold

[tautschnig]

Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way.

We previously attempted to do this in in #6194 (inspired by #2108, but not picking up all its changes), but then reverted the gist of the change in #6232 as array-bug-6230/main.c demonstrated lingering issues. This PR now addresses the flaw in the array theory back-end.

We may still run into performance regressions as the threshold of 1000 bits of total size of the array object is possibly lower than where the cost of bit-blasting exceeds the cost of constraints produced by our current array theory implementation. Two of our existing regression tests already demonstrate this problem, hence those now use --arrays-uf-never.

• 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.
• 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 46.15385% with 7 lines in your changes missing coverage. Please review.

Project coverage is 78.19%. Comparing base (d2b4455) to head (dc4157e).
Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/solvers/flattening/arrays.cpp	46.15%	7 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8468      +/-   ##
===========================================
- Coverage    78.31%   78.19%   -0.12%     
===========================================
  Files         1726     1726              
  Lines       188817   189119     +302     
  Branches     18270    18273       +3     
===========================================
+ Hits        147874   147888      +14     
- Misses       40943    41231     +288     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

Performance benchmarks nicely demonstrate that this change can indeed cause real-world performance problems. Will look into these.