Use array comprehension for large byte_extract lowering

lower_byte_extract_array_vector expands byte_extract of an array
type into an element-by-element array_exprt. For large arrays
(e.g., char[100000] in a union), this creates N sub-expressions
that are each recursively lowered and simplified, resulting in
O(N^2) behavior.

When the array size exceeds MAX_FLATTENED_ARRAY_SIZE (1000), use
array_comprehension_exprt instead. This path already exists for
arrays with non-constant size; now it is also used for large
constant-size arrays. This reduces the lowering from O(N)
expressions to O(1).

Performance on union_large_array (char[100000] in a union):
  Before: >120s with --arrays-uf-always
  After:  2.3s with --arrays-uf-always

Remove thorough-arrays-uf-always tag from union_large_array.desc
since the test now completes in 2 seconds.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

src/util/lower_byte_operators.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "c_types.h"
 #include "endianness_map.h"
 #include "expr_util.h"
+#include "magic.h"
 #include "namespace.h"
 #include "narrow.h"
 #include "pointer_offset_size.h"
@@ -1112,7 +1113,13 @@ static exprt lower_byte_extract_array_vector(
   else
     num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());
 
-  if(num_elements.has_value())
+  // For large arrays, element-by-element expansion creates N expressions
+  // that are each recursively lowered and simplified, resulting in O(N^2)
+  // behaviour. Use array_comprehension_exprt (below) instead, which
+  // represents the same semantics with a single symbolic expression.
+  if(
+    num_elements.has_value() &&
+    (src.type().id() != ID_array || *num_elements <= MAX_FLATTENED_ARRAY_SIZE))
   {
     exprt::operandst operands;
     operands.reserve(*num_elements);