Do not simplify (T)bv-typed when T has smaller bit width

We must not modify the bit width of bv (and not signed/unsigned bv)
typed expressions via type casts. Make sure simplification doesn't give
rise to such expressions.

Fixes: #7426

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1306,9 +1306,20 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     // where T1 has fewer bits than T2
     if(
       op_type_id == expr_type_id &&
-      (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
-       expr_type_id == ID_bv) &&
-      to_bitvector_type(expr_type).get_width() <=
+      (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
+      to_bitvector_type(expr_type).get_width() <
+        to_bitvector_type(operand.type()).get_width() &&
+      to_typecast_expr(operand).op().type().id() != ID_bv)
+    {
+      auto new_expr = expr;
+      new_expr.op() = to_typecast_expr(operand).op();
+      // might enable further simplification
+      return changed(simplify_typecast(new_expr)); // recursive call
+    }
+    else if(
+      op_type_id == ID_bv &&
+      (expr_type_id == ID_signedbv || expr_type_id == ID_unsignedbv) &&
+      to_bitvector_type(expr_type).get_width() ==
         to_bitvector_type(operand.type()).get_width())
     {
       auto new_expr = expr;