Workaround for aarch64 regression test failure

aarch64 has unsigned char by default, and the ensuing type casts trip up
our quantifier instantiation code.

Author: tautschnig

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
 
@@ -14,3 +14,29 @@ int main()
 
   return 0;
 }
+
+#if 0
+We should really teach the simplifier to process
+
+          0: >=
+               * type: bool
+               0: typecast
+                   * type: signedbv
+                       * width: 32
+                   0: zero_extend
+                       * type: unsignedbv
+                           * width: 32
+                       0: symbol
+                           * type: unsignedbv
+                               * width: 8
+                           * identifier: main::1::1::i!0@2#0
+                           * #quoted: 1
+               1: typecast
+                   * type: signedbv
+                       * width: 32
+                   0: constant
+                       * type: unsignedbv
+                           * width: 32
+                       * value: 0
+
+#endif