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