Simplify byte extract: support signed and unsigned offsets

The minimized example from #7357 resulted in an invariant failure in
`solvers/flattening/boolbv_add_sub.cpp`, reporting "add/sub with mixed
types." This was caused by simplifying nested byte-extract operations
where one used unsigned offsets and the other one signed. Since we do
not required a particular type for byte-extract offsets we must cope
with different offset types when folding nested byte-extract operations
into a single one.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1660,8 +1660,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   {
     auto tmp = expr;
 
-    tmp.offset() = simplify_plus(
-      plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset()));
+    tmp.offset() = simplify_rec(plus_exprt(
+      typecast_exprt::conditional_cast(
+        to_byte_extract_expr(expr.op()).offset(), expr.offset().type()),
+      expr.offset()));
     tmp.op() = to_byte_extract_expr(expr.op()).op();
 
     return changed(simplify_byte_extract(tmp)); // recursive call