diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h
index 8920a952f1d..348c245891c 100644
--- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h
+++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h
@@ -45,4 +45,13 @@ enum __gcc_atomic_memmodels {
 };
 
 typedef unsigned char __tile __attribute__ ((__vector_size__ (1024)));
+
+// GCC and Clang use the following on ARM:
+typedef float __Float32x4_t __attribute__ ((__vector_size__ (16)));
+typedef double __Float64x2_t __attribute__ ((__vector_size__ (16)));
+// The following ARM (scalable vector) extensions define vectors the size of
+// which is not known at compile time.
+typedef float *__SVFloat32_t;
+typedef double *__SVFloat64_t;
+typedef __CPROVER_bool *__SVBool_t;
 // clang-format on