byte-operators unpack_rec: enforce max-bytes if supplied

Otherwise it may return more bytes than were requested, leading to an invariant violation in lower_byte_update
which passes a constant limit and enforces that it is obeyed.

Also remove the broken-smt-backend tag from tests which now pass.

Author: smowton

regression/cbmc/byte_update14/test.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc;
+  ptr[argc] = 'a';
+  ptr[1] = (char)argc;
+  assert(ptr[1] == (char)argc);
+  assert(array[1] == (char)argc);
+}

regression/cbmc/byte_update14/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 10.*SUCCESS$
+^\[main.assertion\.2\] line 11.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$

regression/cbmc/dynamic_size1/stack_object.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 stack_object.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
 ^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$

src/solvers/lowering/byte_operators.cpp

@@ -583,11 +583,24 @@ static exprt unpack_array_vector(
 
     // recursively unpack each element so that we eventually just have an array
     // of bytes left
-    exprt sub = unpack_rec(element, little_endian, {}, max_bytes, ns, true);
+
+    const optionalt<mp_integer> element_max_bytes =
+      max_bytes
+        ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
+        : optionalt<mp_integer>{};
+    const std::size_t element_max_bytes_int =
+      element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
+                        : el_bytes;
+
+    exprt sub =
+      unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
     exprt::operandst sub_operands =
-      instantiate_byte_array(sub, 0, el_bytes, ns);
+      instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
     byte_operands.insert(
       byte_operands.end(), sub_operands.begin(), sub_operands.end());
+
+    if(max_bytes && byte_operands.size() >= *max_bytes)
+      break;
   }
 
   const std::size_t size = byte_operands.size();
@@ -926,10 +939,21 @@ static exprt unpack_rec(
     // endianness
     auto bits_opt = pointer_offset_bits(src.type(), ns);
     DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
+
     mp_integer bits = *bits_opt;
+    mp_integer i = 0;
+
+    if(max_bytes.has_value())
+    {
+      const auto max_bits = *max_bytes * 8;
+      if(little_endian)
+        bits = std::min(bits, max_bits);
+      else
+        i = std::max(mp_integer{0}, bits - max_bits);
+    }
 
     exprt::operandst byte_operands;
-    for(mp_integer i=0; i<bits; i+=8)
+    for(; i < bits; i += 8)
     {
       extractbits_exprt extractbits(
         typecast_exprt::conditional_cast(