diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-3.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-3.h
index faaad75fd87..19688305512 100644
--- a/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-3.h
+++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-3.h
@@ -99,7 +99,7 @@ void __builtin_ia32_pmovusdw256mem_mask(__gcc_v8hi*, __gcc_v8si, unsigned char);
 void __builtin_ia32_pmovusdw128mem_mask(unsigned long long int *, __gcc_v4si, unsigned char);
 unsigned int __builtin_ia32_rdpkru(void);
 void __builtin_ia32_wrpkru(unsigned int);
-__gcc_v8si __builtin_ia32_vec_pack_sfix256 (__gcc_v4df, __gcc_v4df);
+__gcc_v8si __builtin_ia32_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
 unsigned short __builtin_ia32_lzcnt_u16(unsigned short);
 unsigned short __builtin_ia32_tzcnt_u16(unsigned short);
 unsigned int __builtin_ia32_tzcnt_u32(unsigned int);
diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h
index 0ca2336a8d7..b3e479c6b11 100644
--- a/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h
+++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h
@@ -768,7 +768,7 @@ unsigned int __builtin_ia32_rdrand32_step(unsigned int*);
 unsigned int __builtin_ia32_rdrand64_step(unsigned long long int *);
 void __builtin_ia32_movntsd(double*, __gcc_v2df);
 void __builtin_ia32_movntss(float*, __gcc_v4sf);
-__gcc_v2di __builtin_ia32_extrq (__gcc_v2di, __gcc_v16qi);
+__gcc_v2di __builtin_ia32_extrq(__gcc_v2di, __gcc_v16qi);
 __gcc_v2di __builtin_ia32_extrqi(__gcc_v2di, unsigned int, unsigned int);
 __gcc_v2di __builtin_ia32_insertq(__gcc_v2di, __gcc_v2di);
 __gcc_v2di __builtin_ia32_insertqi(__gcc_v2di, __gcc_v2di, unsigned int, unsigned int);
@@ -912,10 +912,10 @@ __gcc_v2df __builtin_ia32_fnmsubpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
 __gcc_v4sf __builtin_ia32_fnmsubps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
 __gcc_v2df __builtin_ia32_fnmsubsd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
 __gcc_v4sf __builtin_ia32_fnmsubss(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
-__gcc_v2df __builtin_ia32_fmaddsubpd (__gcc_v2df, __gcc_v2df, __gcc_v2df);
-__gcc_v4sf __builtin_ia32_fmaddsubps (__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
-__gcc_v2df __builtin_ia32_fmsubaddpd (__gcc_v2df, __gcc_v2df, __gcc_v2df);
-__gcc_v4sf __builtin_ia32_fmsubaddps (__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
+__gcc_v2df __builtin_ia32_fmaddsubpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
+__gcc_v4sf __builtin_ia32_fmaddsubps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
+__gcc_v2df __builtin_ia32_fmsubaddpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
+__gcc_v4sf __builtin_ia32_fmsubaddps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
 __gcc_v4df __builtin_ia32_fmaddpd256(__gcc_v4df, __gcc_v4df, __gcc_v4df);
 __gcc_v8sf __builtin_ia32_fmaddps256(__gcc_v8sf, __gcc_v8sf, __gcc_v8sf);
 __gcc_v4df __builtin_ia32_fmsubpd256(__gcc_v4df, __gcc_v4df, __gcc_v4df);
diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_mem_string.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_mem_string.h
index 179b25660ba..90410c48c40 100644
--- a/src/ansi-c/compiler_headers/gcc_builtin_headers_mem_string.h
+++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_mem_string.h
@@ -29,7 +29,7 @@ char* __builtin___strncat_chk(char*, const char*, __CPROVER_size_t, __CPROVER_si
 char* __builtin___strncpy_chk(char*, const char*, __CPROVER_size_t, __CPROVER_size_t);
 int __builtin___vfprintf_chk(void*, int, const char*, __builtin_va_list);
 int __builtin___vprintf_chk(int, const char*, __builtin_va_list);
-int __builtin___vsnprintf_chk (char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
+int __builtin___vsnprintf_chk(char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
 int __builtin___vsprintf_chk(char*, int, __CPROVER_size_t, const char*, __builtin_va_list);
 void* __builtin_aggregate_incoming_address();
 void* __builtin_aligned_alloc(__CPROVER_size_t, __CPROVER_size_t);