diff --git a/regression/cbmc/Quantifiers-type2/main.c b/regression/cbmc/Quantifiers-type2/main.c
index 73bd1913906..bdc3fd74cc9 100644
--- a/regression/cbmc/Quantifiers-type2/main.c
+++ b/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
 
diff --git a/regression/cbmc/Quantifiers-type2/unsigned-char.c b/regression/cbmc/Quantifiers-type2/unsigned-char.c
new file mode 100644
index 00000000000..186c763950b
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/Quantifiers-type2/unsigned-char.desc b/regression/cbmc/Quantifiers-type2/unsigned-char.desc
new file mode 100644
index 00000000000..603f48f7a32
--- /dev/null
+++ b/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
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 1eaa54a4dea..a0eb1b9dd89 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -975,6 +975,52 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       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
+        }
+      }
     }
   }