4typedef int __gcc_m64
__attribute__ ((__vector_size__ (8), __may_alias__));
7typedef char __gcc_v16qi
__attribute__ ((__vector_size__ (16)));
8typedef char __gcc_v32qi
__attribute__ ((__vector_size__ (32)));
9typedef char __gcc_v64qi
__attribute__ ((__vector_size__ (64)));
13typedef int __gcc_v16si
__attribute__ ((__vector_size__ (64)));
14typedef int __gcc_v256si
__attribute__ ((__vector_size__ (1024)));
15typedef short __gcc_v4hi
__attribute__ ((__vector_size__ (8)));
16typedef short __gcc_v8hi
__attribute__ ((__vector_size__ (16)));
17typedef short __gcc_v16hi
__attribute__ ((__vector_size__ (32)));
18typedef short __gcc_v32hi
__attribute__ ((__vector_size__ (64)));
19typedef __CPROVER_Float16 __gcc_v8hf
__attribute__ ((__vector_size__ (16)));
20typedef __CPROVER_Float16 __gcc_v16hf
__attribute__ ((__vector_size__ (32)));
21typedef __CPROVER_Float16 __gcc_v32hf
__attribute__ ((__vector_size__ (64)));
22typedef float __gcc_v2sf
__attribute__ ((__vector_size__ (8)));
23typedef float __gcc_v4sf
__attribute__ ((__vector_size__ (16)));
24typedef float __gcc_v8sf
__attribute__ ((__vector_size__ (32)));
25typedef float __gcc_v16sf
__attribute__ ((__vector_size__ (64)));
26typedef double __gcc_v2df
__attribute__ ((__vector_size__ (16)));
27typedef double __gcc_v4df
__attribute__ ((__vector_size__ (32)));
28typedef double __gcc_v8df
__attribute__ ((__vector_size__ (64)));
29typedef long long __gcc_v1di
__attribute__ ((__vector_size__ (8)));
30typedef long long __gcc_v2di
__attribute__ ((__vector_size__ (16)));
31typedef long long __gcc_v4di
__attribute__ ((__vector_size__ (32)));
32typedef long long __gcc_v8di
__attribute__ ((__vector_size__ (64)));
33typedef unsigned short __gcc_v32uhi
__attribute__ ((__vector_size__ (64)));
34typedef unsigned int __gcc_v4usi
__attribute__ ((__vector_size__ (16)));
35typedef unsigned int __gcc_v8usi
__attribute__ ((__vector_size__ (32)));
36typedef unsigned int __gcc_v16usi
__attribute__ ((__vector_size__ (64)));
38typedef unsigned long long __gcc_v2udi
__attribute__ ((__vector_size__ (16)));
39typedef unsigned long long __gcc_v4udi
__attribute__ ((__vector_size__ (32)));
40typedef unsigned long long __gcc_v8udi
__attribute__ ((__vector_size__ (64)));
46typedef unsigned char __tile
__attribute__ ((__vector_size__ (1024)));
49typedef float __Float32x4_t
__attribute__ ((__vector_size__ (16)));
50typedef double __Float64x2_t
__attribute__ ((__vector_size__ (16)));