Simplify typecast of zero-extension to just a typecast

regression/cbmc/Quantifiers-type2/main.c

@@ -5,7 +5,7 @@ int main()
 
   // clang-format off
   // clang-format would rewrite the "==>" as "== >"
-  __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { signed char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
   __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
   // clang-format on
 

regression/cbmc/Quantifiers-type2/unsigned-char.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int b[2];
+  int c[2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assume( __CPROVER_forall { unsigned char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
+  // clang-format on
+
+  assert(b[0] == 10 && b[1] == 10);
+  assert(c[0] == 10 && c[1] == 10);
+
+  return 0;
+}

regression/cbmc/Quantifiers-type2/unsigned-char.desc

@@ -0,0 +1,11 @@
+CORE no-new-smt
+unsigned-char.c
+
+^\*\* Results:$
+^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
+^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/simplify_expr.cpp

@@ -975,6 +975,52 @@
       else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
       {
       }
+      else if(op_id == ID_zero_extend)
+      {
+        const exprt &zero_extended_op = to_zero_extend_expr(expr.op());
+        if(
+          auto bv_type =
+            type_try_dynamic_cast<bitvector_typet>(zero_extended_op.type()))
+        {
+          auto new_expr = expr;
+          if(
+            bv_type->id() == ID_signedbv &&
+            bv_type->get_width() < to_bitvector_type(expr_type).get_width())
+          {
+            new_expr.op() =
+              simplify_typecast(
+                typecast_exprt{
+                  zero_extended_op, unsignedbv_typet{bv_type->get_width()}})
+                .expr;
+          }
+          else
+            new_expr.op() = zero_extended_op;
+          return changed(simplify_typecast(new_expr)); // rec. call
+        }
+      }
+      else if(op_id == ID_concatenation)
+      {
+        const auto &operands = expr.op().operands();
+        if(
+          operands.size() == 2 && operands.front().is_constant() &&
+          to_constant_expr(operands.front()).value_is_zero_string())
+        {
+          auto new_expr = expr;
+          const bitvector_typet &bv_type =
+            to_bitvector_type(operands.back().type());
+          if(bv_type.id() == ID_signedbv)
+          {
+            new_expr.op() =
+              simplify_typecast(
+                typecast_exprt{
+                  operands.back(), unsignedbv_typet{bv_type.get_width()}})
+                .expr;
+          }
+          else
+            new_expr.op() = operands.back();
+          return changed(simplify_typecast(new_expr)); // rec. call
+        }
+      }
     }
   }