byte_extract lowering of arrays: optimise for constant index

No need to construct index_exprt when we can just pick the operand out of a
vector.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -499,8 +499,21 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       little_endian?(width_bytes-i-1):i;
 
     plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
-    index_exprt index_expr(root, offset_i);
-    op.push_back(index_expr);
+    simplify(offset_i, ns);
+
+    mp_integer index = 0;
+    if(
+      !offset_i.is_constant() ||
+      (root.id() != ID_array && root.id() != ID_vector) ||
+      to_integer(to_constant_expr(offset_i), index) ||
+      index >= root.operands().size() || index < 0)
+    {
+      op.push_back(index_exprt(root, offset_i));
+    }
+    else
+    {
+      op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
+    }
   }
 
   if(width_bytes==1)