diff --git a/regression/cbmc/Variadic1/test.desc b/regression/cbmc/Variadic1/test.desc
index aea17ee4da8..9efefbc7362 100644
--- a/regression/cbmc/Variadic1/test.desc
+++ b/regression/cbmc/Variadic1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/va_list3/test.desc b/regression/cbmc/va_list3/test.desc
index 52168c7eba4..39d9265e8a7 100644
--- a/regression/cbmc/va_list3/test.desc
+++ b/regression/cbmc/va_list3/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/va_list3/windows-preprocessed.desc b/regression/cbmc/va_list3/windows-preprocessed.desc
new file mode 100644
index 00000000000..9049dd0fdfa
--- /dev/null
+++ b/regression/cbmc/va_list3/windows-preprocessed.desc
@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+windows-preprocessed.i
+--winx64
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The preprocessed file was generated from va_list3/main.c using Visual Studio
+2017.
diff --git a/regression/cbmc/va_list3/windows-preprocessed.i b/regression/cbmc/va_list3/windows-preprocessed.i
new file mode 100755
index 00000000000..a47c0cde2ca
--- /dev/null
+++ b/regression/cbmc/va_list3/windows-preprocessed.i
@@ -0,0 +1,5873 @@
+#line 1 "main.c"
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\stdarg.h"
+
+
+
+
+
+
+
+#pragma once
+
+
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+#pragma once
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    
+#line 29 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+    
+    
+
+#line 39 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+        
+
+
+            
+        #line 44 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+    #line 45 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 46 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+#pragma once
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 151 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+#line 155 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 185 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+#line 188 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+#line 190 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+#line 196 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+#line 200 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+#line 207 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+#line 219 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+#line 228 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+#line 229 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#pragma region Input Buffer SAL 1 compatibility macros
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#pragma endregion Input Buffer SAL 1 compatibility macros
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1555 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1586 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1611 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1624 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1663 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1775 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1878 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2047 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2149 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2366 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+#line 2367 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2595 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+
+    
+    
+    
+    
+
+    
+    
+
+#line 2634 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2868 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+#line 2878 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+    
+    
+#line 2883 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+#line 2890 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+#line 2891 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+#line 2898 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+#line 2899 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+#line 2911 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 2945 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\concurrencysal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#pragma once
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 265 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\concurrencysal.h"
+
+
+
+#line 269 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\concurrencysal.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 352 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\concurrencysal.h"
+
+
+
+
+
+#line 358 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\concurrencysal.h"
+#line 2971 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\sal.h"
+
+#line 48 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 1 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+
+
+
+#pragma once
+
+
+
+#pragma pack(push, 8)
+
+
+
+
+
+
+
+#line 24 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+    
+    
+        typedef unsigned __int64  uintptr_t;
+    
+
+#line 32 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+#line 33 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+    
+    
+
+
+        typedef char* va_list;
+    #line 41 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+#line 42 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+    
+#line 48 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+#line 54 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+#line 58 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+    
+    
+#line 61 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+
+
+
+
+#line 73 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+#line 81 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+
+
+
+
+#line 93 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+#line 99 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+
+
+
+
+#line 111 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+    void __cdecl __va_start(va_list* , ...);
+
+    
+    
+
+
+
+    
+
+#line 122 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 159 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+    
+
+#line 163 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vadefs.h"
+
+#pragma pack(pop)
+#line 49 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 64 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+
+
+#line 74 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+    
+
+
+    
+
+
+#line 82 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+__pragma(pack(push, 8))
+
+
+
+
+    
+
+
+        
+    #line 93 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 94 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    
+
+#line 113 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+#line 115 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+        
+    #line 117 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 118 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+
+#line 123 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+        
+    #line 125 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 126 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+#line 132 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+    
+    
+#line 135 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+    
+#line 141 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+
+    
+
+
+#line 153 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+#line 157 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+    
+#line 159 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+    
+#line 165 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+
+
+
+      
+    #line 173 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 174 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+    typedef unsigned __int64 size_t;
+    typedef __int64          ptrdiff_t;
+    typedef __int64          intptr_t;
+
+
+
+
+#line 188 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+#line 192 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+#line 196 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+    typedef _Bool __vcrt_bool;
+#line 198 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+    
+#line 203 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+#line 207 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+#line 211 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+    
+    typedef unsigned short wchar_t;
+#line 217 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+
+
+        
+    #line 224 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 225 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+
+
+#line 231 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+
+
+
+
+    
+#line 243 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+
+
+
+#line 250 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+
+
+        
+
+
+
+
+    #line 261 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 262 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+
+#line 266 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    
+        
+    
+
+
+#line 274 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 275 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+
+    void __cdecl __security_init_cookie(void);
+
+    
+
+
+
+        void __cdecl __security_check_cookie(  uintptr_t _StackCookie);
+        __declspec(noreturn) void __cdecl __report_gsfailure(  uintptr_t _StackCookie);
+    #line 286 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 287 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+extern uintptr_t __security_cookie;
+
+
+    
+    
+    
+#line 295 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+
+__pragma(pack(pop))
+
+#line 299 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\vcruntime.h"
+#line 12 "C:\\Program Files (x86)\\Microsoft Visual Studio\\2017\\Community\\VC\\Tools\\MSVC\\14.14.26428\\include\\stdarg.h"
+
+__pragma(pack(push, 8))
+
+
+
+
+
+
+
+
+
+
+__pragma(pack(pop))
+#line 2 "main.c"
+#line 1 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\assert.h"
+
+
+
+
+
+
+
+
+
+#line 11 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\assert.h"
+
+#line 1 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+#pragma once
+
+
+
+__pragma(pack(push, 8))
+
+
+
+
+
+
+
+
+
+    
+
+#line 25 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+#line 27 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+        
+    #line 29 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 30 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+    
+#line 36 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+#line 41 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+#line 43 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+        
+    #line 45 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 46 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 50 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 52 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+#line 58 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+#line 64 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 66 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+    
+#line 73 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 77 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 79 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+    
+
+
+        
+    #line 97 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 98 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 102 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 104 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 108 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 110 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 114 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+#line 116 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 141 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 145 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    typedef _Bool __crt_bool;
+#line 147 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+    
+#line 159 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    
+
+#line 181 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+        
+    #line 183 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 184 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 188 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+#line 192 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+    
+
+
+
+
+
+
+
+
+
+
+
+        
+    #line 215 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 216 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+#line 220 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+        
+    
+
+#line 227 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 228 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ void __cdecl _invalid_parameter_noinfo(void);
+ __declspec(noreturn) void __cdecl _invalid_parameter_noinfo_noreturn(void);
+
+__declspec(noreturn)
+ void __cdecl _invoke_watson(
+      wchar_t const* _Expression,
+      wchar_t const* _FunctionName,
+      wchar_t const* _FileName,
+            unsigned int _LineNo,
+            uintptr_t _Reserved);
+
+
+    
+
+
+
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+
+    #line 283 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 284 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 301 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+        
+
+
+    #line 310 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 311 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+    
+
+
+
+
+
+
+        
+    #line 329 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 330 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+        
+    #line 337 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 338 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 342 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 356 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 372 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+    
+#line 379 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 383 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+#line 388 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 389 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+        
+
+
+            
+        #line 399 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    #line 400 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 401 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 405 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+#line 411 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+        
+
+
+
+    #line 421 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 422 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+        
+    
+
+
+
+#line 431 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+    
+        
+        
+        
+    
+
+
+
+#line 441 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+    
+        
+              
+        
+
+#line 448 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    
+
+
+
+#line 453 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+    
+        
+    
+
+
+
+#line 461 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+    
+        
+    
+
+
+
+#line 469 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 470 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+#line 474 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+typedef int                           errno_t;
+typedef unsigned short                wint_t;
+typedef unsigned short                wctype_t;
+typedef long                          __time32_t;
+typedef __int64                       __time64_t;
+
+typedef struct __crt_locale_data_public
+{
+      unsigned short const* _locale_pctype;
+      int _locale_mb_cur_max;
+               unsigned int _locale_lc_codepage;
+} __crt_locale_data_public;
+
+typedef struct __crt_locale_pointers
+{
+    struct __crt_locale_data*    locinfo;
+    struct __crt_multibyte_data* mbcinfo;
+} __crt_locale_pointers;
+
+typedef __crt_locale_pointers* _locale_t;
+
+typedef struct _Mbstatet
+{ 
+    unsigned long _Wchar;
+    unsigned short _Byte, _State;
+} _Mbstatet;
+
+typedef _Mbstatet mbstate_t;
+
+
+
+#line 514 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+#line 518 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    
+
+
+        typedef __time64_t time_t;
+    #line 525 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 526 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+    
+#line 531 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+    typedef size_t rsize_t;
+#line 535 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 696 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+
+    #line 711 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 712 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1787 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+        
+        
+        
+        
+
+        
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+
+            
+
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+            
+
+
+
+            
+
+
+
+            
+
+
+
+            
+
+
+            
+
+
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+            
+
+
+
+
+            
+
+        
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#line 1977 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+    #line 1978 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+#line 1979 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\corecrt.h"
+
+
+
+__pragma(pack(pop))
+#line 13 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\assert.h"
+
+__pragma(pack(push, 8))
+
+
+
+
+
+
+
+
+
+
+
+     void __cdecl _wassert(
+          wchar_t const* _Message,
+          wchar_t const* _File,
+            unsigned       _Line
+        );
+
+    
+
+
+
+
+#line 38 "C:\\Program Files (x86)\\Windows Kits\\10\\include\\10.0.17134.0\\ucrt\\assert.h"
+
+
+
+__pragma(pack(pop))
+#line 3 "main.c"
+
+void foo(int n, ...);
+
+int main()
+{
+  foo(1, 1u);
+  foo(2, 2l);
+  foo(3, 3.0);
+  return 0;
+}
+
+void foo(int n, ...)
+{
+  va_list vl;
+
+  ((void)(__va_start(&vl, n)));
+  
+  switch(n)
+  {
+  case 1: (void)( (!!(((sizeof(unsigned) > sizeof(__int64) || (sizeof(unsigned) & (sizeof(unsigned) - 1)) != 0) ? **(unsigned**)((vl += sizeof(__int64)) - sizeof(__int64)) : *(unsigned* )((vl += sizeof(__int64)) - sizeof(__int64)))==1)) || (_wassert(L"va_arg(vl, unsigned)==1", L"main.c", (unsigned)(22)), 0) ); break;
+  case 2: (void)( (!!(((sizeof(long) > sizeof(__int64) || (sizeof(long) & (sizeof(long) - 1)) != 0) ? **(long**)((vl += sizeof(__int64)) - sizeof(__int64)) : *(long* )((vl += sizeof(__int64)) - sizeof(__int64)))==2)) || (_wassert(L"va_arg(vl, long)==2", L"main.c", (unsigned)(23)), 0) ); break;
+  case 3: (void)( (!!(((sizeof(double) > sizeof(__int64) || (sizeof(double) & (sizeof(double) - 1)) != 0) ? **(double**)((vl += sizeof(__int64)) - sizeof(__int64)) : *(double* )((vl += sizeof(__int64)) - sizeof(__int64)))==3.0)) || (_wassert(L"va_arg(vl, double)==3.0", L"main.c", (unsigned)(24)), 0) ); break;
+  }
+  
+  ((void)(vl = (va_list)0));
+}
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 87f015488e4..80d02a6bf2f 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -573,10 +573,6 @@ std::string expr2ct::convert_rec(
 
     return q+dest+d;
   }
-  else if(src.id()==ID_gcc_builtin_va_list)
-  {
-    return q+"__builtin_va_list"+d;
-  }
   else if(src.id()==ID_constructor ||
           src.id()==ID_destructor)
   {
@@ -3621,8 +3617,8 @@ std::string expr2ct::convert_with_precedence(
       return convert_prob_uniform(src, precedence=16);
     else if(statement==ID_statement_expression)
       return convert_statement_expression(src, precedence=15);
-    else if(statement==ID_gcc_builtin_va_arg_next)
-      return convert_function(src, "gcc_builtin_va_arg_next");
+    else if(statement == ID_va_start)
+      return convert_function(src, CPROVER_PREFIX "va_start");
     else
       return convert_norep(src, precedence);
   }
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index c822e2e843a..9c28026fca9 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -104,9 +104,10 @@ void goto_program2codet::scan_for_varargs()
       const exprt &l = target->get_assign().lhs();
       const exprt &r = target->get_assign().rhs();
 
-      // find va_arg_next
-      if(r.id()==ID_side_effect &&
-         to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
+      // find va_start
+      if(
+        r.id() == ID_side_effect &&
+        to_side_effect_expr(r).get_statement() == ID_va_start)
       {
         assert(r.has_operands());
         va_list_expr.insert(r.op0());
@@ -121,24 +122,7 @@ void goto_program2codet::scan_for_varargs()
     }
 
   if(!va_list_expr.empty())
-  {
     system_headers.insert("stdarg.h");
-
-    code_typet &code_type=
-      to_code_type(symbol_table.get_writeable_ref(func_name).type);
-    code_typet::parameterst &parameters=code_type.parameters();
-
-    for(code_typet::parameterst::iterator
-        it2=parameters.begin();
-        it2!=parameters.end();
-        ++it2)
-    {
-      const symbol_exprt arg=
-        ns.lookup(it2->get_identifier()).symbol_expr();
-      if(va_list_expr.find(arg)!=va_list_expr.end())
-        it2->type().id(ID_gcc_builtin_va_list);
-    }
-  }
 }
 
 goto_programt::const_targett goto_program2codet::convert_instruction(
@@ -322,26 +306,24 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
     code_function_callt f(
       symbol_exprt("va_end", code_typet({}, empty_typet())),
       {this_va_list_expr});
-    f.arguments().back().type().id(ID_gcc_builtin_va_list);
 
     dest.add(std::move(f));
   }
-  else if(r.id()==ID_address_of)
+  else if(
+    r.id() == ID_side_effect &&
+    to_side_effect_expr(r).get_statement() == ID_va_start)
   {
     code_function_callt f(
-      symbol_exprt("va_start", code_typet({}, empty_typet())),
-      {this_va_list_expr, to_address_of_expr(r).object()});
-    f.arguments().front().type().id(ID_gcc_builtin_va_list);
+      symbol_exprt(ID_va_start, code_typet({}, empty_typet())),
+      {this_va_list_expr, to_address_of_expr(skip_typecast(r.op0())).object()});
 
     dest.add(std::move(f));
   }
-  else if(r.id()==ID_side_effect &&
-          to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
+  else if(r.id() == ID_plus)
   {
     code_function_callt f(
       symbol_exprt("va_arg", code_typet({}, empty_typet())),
       {this_va_list_expr});
-    f.arguments().back().type().id(ID_gcc_builtin_va_list);
 
     // we do not bother to set the correct types here, they are not relevant for
     // generating the correct dumped output
@@ -394,7 +376,6 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
     code_function_callt f(
       symbol_exprt("va_copy", code_typet({}, empty_typet())),
       {this_va_list_expr, r});
-    f.arguments().front().type().id(ID_gcc_builtin_va_list);
 
     dest.add(std::move(f));
   }
@@ -1452,9 +1433,6 @@ void goto_program2codet::cleanup_code(
 {
   if(code.get_statement()==ID_decl)
   {
-    if(va_list_expr.find(code.op0())!=va_list_expr.end())
-      code.op0().type().id(ID_gcc_builtin_va_list);
-
     if(code.operands().size()==2 &&
        code.op1().id()==ID_side_effect &&
        to_side_effect_expr(code.op1()).get_statement()==ID_function_call)
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 93db4755b84..815c671f1bd 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1080,10 +1080,10 @@ void goto_convertt::do_function_call_symbol(
   else if(identifier==ID_gcc_builtin_va_arg)
   {
     // This does two things.
-    // 1) Move list pointer to next argument.
-    //    Done by gcc_builtin_va_arg_next.
-    // 2) Return value of argument.
+    // 1) Return value of argument.
     //    This is just dereferencing.
+    // 2) Move list pointer to next argument.
+    //    This is just an increment.
 
     if(arguments.size()!=1)
     {
@@ -1095,25 +1095,21 @@ void goto_convertt::do_function_call_symbol(
 
     exprt list_arg=make_va_list(arguments[0]);
 
-    {
-      side_effect_exprt rhs(
-        ID_gcc_builtin_va_arg_next,
-        list_arg.type(),
-        function.source_location());
-      rhs.copy_to_operands(list_arg);
-      rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
-      dest.add(goto_programt::make_assignment(
-        list_arg, rhs, function.source_location()));
-    }
-
     if(lhs.is_not_nil())
     {
       typet t=pointer_type(lhs.type());
-      dereference_exprt rhs(typecast_exprt(list_arg, t), lhs.type());
+      dereference_exprt rhs{typecast_exprt(dereference_exprt{list_arg}, t)};
       rhs.add_source_location()=function.source_location();
       dest.add(
         goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
+
+    code_assignt assign{
+      list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
+    assign.rhs().set(
+      ID_C_va_arg_type, to_code_type(function.type()).return_type());
+    dest.add(goto_programt::make_assignment(
+      std::move(assign), function.source_location()));
   }
   else if(identifier=="__builtin_va_copy")
   {
@@ -1138,7 +1134,7 @@ void goto_convertt::do_function_call_symbol(
     dest.add(goto_programt::make_assignment(
       dest_expr, src_expr, function.source_location()));
   }
-  else if(identifier=="__builtin_va_start")
+  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
   {
     // Set the list argument to be the address of the
     // parameter argument.
@@ -1151,8 +1147,6 @@ void goto_convertt::do_function_call_symbol(
     }
 
     exprt dest_expr=make_va_list(arguments[0]);
-    const typecast_exprt src_expr(
-      address_of_exprt(arguments[1]), dest_expr.type());
 
     if(!is_lvalue(dest_expr))
     {
@@ -1161,8 +1155,13 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
+    side_effect_exprt rhs{
+      ID_va_start, dest_expr.type(), function.source_location()};
+    rhs.add_to_operands(
+      typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
+
     dest.add(goto_programt::make_assignment(
-      dest_expr, src_expr, function.source_location()));
+      std::move(dest_expr), std::move(rhs), function.source_location()));
   }
   else if(identifier=="__builtin_va_end")
   {
diff --git a/src/goto-symex/frame.h b/src/goto-symex/frame.h
index 09b91269f5d..94a00d37c31 100644
--- a/src/goto-symex/frame.h
+++ b/src/goto-symex/frame.h
@@ -26,6 +26,7 @@ struct framet
   irep_idt function_identifier;
   std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
   symex_targett::sourcet calling_location;
+  std::vector<irep_idt> parameter_names;
 
   goto_programt::const_targett end_of_function;
   exprt return_value = nil_exprt();
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index b0fda713b7d..8e6965c9d88 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -610,10 +610,9 @@ class goto_symext
   /// \return The resulting expression
   static exprt add_to_lhs(const exprt &lhs, const exprt &what);
 
-  virtual void symex_gcc_builtin_va_arg_next(
-    statet &state,
-    const exprt &lhs,
-    const side_effect_exprt &code);
+  virtual void
+  symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
+
   /// Symbolically execute an assignment instruction that has an `allocate` on
   /// the right hand side
   /// \param state: Symbolic execution state for current instruction
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c1117be4ed1..fb996c20f49 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -52,8 +52,8 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
       PRECONDITION(lhs.is_nil());
       symex_printf(state, side_effect_expr);
     }
-    else if(statement==ID_gcc_builtin_va_arg_next)
-      symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
+    else if(statement == ID_va_start)
+      symex_va_start(state, lhs, side_effect_expr);
     else
       UNREACHABLE;
   }
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 4bbd2a43d81..c457a0e4108 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant_utils.h>
 #include <util/optional.h>
 #include <util/pointer_offset_size.h>
@@ -206,24 +208,44 @@ void goto_symext::symex_allocate(
     code_assignt(lhs, typecast_exprt::conditional_cast(rhs, lhs.type())));
 }
 
-irep_idt get_symbol(const exprt &src)
+/// Construct an entry for the var args array. Visual Studio complicates this as
+/// we need to put immediate values or pointers in there, depending on the size
+/// of the parameter.
+static exprt va_list_entry(
+  const irep_idt &parameter,
+  const pointer_typet &lhs_type,
+  const namespacet &ns)
 {
-  if(src.id()==ID_typecast)
-    return get_symbol(to_typecast_expr(src).op());
-  else if(src.id()==ID_address_of)
+  static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
+
+  symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
+
+  // Visual Studio has va_list == char* and stores parameters of size no
+  // greater than the size of a pointer as immediate values
+  if(lhs_type.subtype().id() != ID_pointer)
   {
-    exprt op=to_address_of_expr(src).object();
-    if(op.id()==ID_symbol &&
-       op.get_bool(ID_C_SSA_symbol))
-      return to_ssa_expr(op).get_object_name();
-    else
-      return irep_idt();
+    auto parameter_size = size_of_expr(parameter_expr.type(), ns);
+    CHECK_RETURN(parameter_size.has_value());
+
+    binary_predicate_exprt fits_slot{
+      *parameter_size,
+      ID_le,
+      from_integer(lhs_type.get_width(), parameter_size->type())};
+
+    return if_exprt{
+      fits_slot,
+      typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
+      typecast_exprt::conditional_cast(
+        address_of_exprt{parameter_expr}, void_ptr_type)};
   }
   else
-    return irep_idt();
+  {
+    return typecast_exprt::conditional_cast(
+      address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
+  }
 }
 
-void goto_symext::symex_gcc_builtin_va_arg_next(
+void goto_symext::symex_va_start(
   statet &state,
   const exprt &lhs,
   const side_effect_exprt &code)
@@ -233,42 +255,52 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  // to allow constant propagation
-  exprt tmp = state.rename(code.op0(), ns).get();
-  do_simplify(tmp);
-  irep_idt id=get_symbol(tmp);
-
-  const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
-  CHECK_RETURN(zero.has_value());
-  exprt rhs(*zero);
+  // create an array holding pointers to the parameters, starting after the
+  // parameter that the operand points to
+  const exprt &op = skip_typecast(code.op0());
+  // this must be the address of a symbol
+  const irep_idt start_parameter =
+    to_ssa_expr(to_address_of_expr(op).object()).get_object_name();
 
-  if(!id.empty())
+  exprt::operandst va_arg_operands;
+  bool parameter_id_found = false;
+  for(auto &parameter : state.call_stack().top().parameter_names)
   {
-    // strip last name off id to get function name
-    std::size_t pos=id2string(id).rfind("::");
-    if(pos!=std::string::npos)
+    if(!parameter_id_found)
     {
-      irep_idt function_identifier=std::string(id2string(id), 0, pos);
-      std::string base=id2string(function_identifier)+"::va_arg";
-
-      if(has_prefix(id2string(id), base))
-        id=base+std::to_string(
-          safe_string2unsigned(
-            std::string(id2string(id), base.size(), std::string::npos))+1);
-      else
-        id=base+"0";
-
-      const symbolt *symbol;
-      if(!ns.lookup(id, symbol))
-      {
-        const symbol_exprt symbol_expr(symbol->name, symbol->type);
-        rhs = typecast_exprt::conditional_cast(
-          address_of_exprt(symbol_expr), lhs.type());
-      }
+      parameter_id_found = parameter == start_parameter;
+      continue;
     }
-  }
 
-  symex_assign(state, code_assignt(lhs, rhs));
+    va_arg_operands.push_back(
+      va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
+  }
+  const std::size_t va_arg_size = va_arg_operands.size();
+  exprt array =
+    array_exprt{std::move(va_arg_operands),
+                array_typet{pointer_type(empty_typet{}),
+                            from_integer(va_arg_size, size_type())}};
+
+  symbolt &va_array = get_fresh_aux_symbol(
+    array.type(),
+    id2string(state.source.function_id),
+    "va_args",
+    state.source.pc->source_location,
+    ns.lookup(state.source.function_id).mode,
+    state.symbol_table);
+  va_array.value = array;
+
+  clean_expr(array, state, false);
+  array = state.rename(std::move(array), ns).get();
+  do_simplify(array);
+  symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
+
+  exprt rhs = address_of_exprt{
+    index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
+  rhs = state.rename(std::move(rhs), ns).get();
+  symex_assign(
+    state,
+    code_assignt{lhs, typecast_exprt::conditional_cast(rhs, lhs.type())});
 }
 
 irep_idt get_string_argument_rec(const exprt &src)
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 25fcd5bc0a0..6fd373bb1ee 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/range.h>
@@ -47,6 +48,7 @@ void goto_symext::parameter_assignments(
   {
     INVARIANT(
       !identifier.empty(), "function parameter must have an identifier");
+    state.call_stack().top().parameter_names.push_back(identifier);
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
@@ -147,30 +149,20 @@ void goto_symext::parameter_assignments(
   if(function_type.has_ellipsis())
   {
     // These are va_arg arguments; their types may differ from call to call
-    std::size_t va_count=0;
-    const symbolt *va_sym=nullptr;
-    while(!ns.lookup(
-        id2string(function_identifier)+"::va_arg"+std::to_string(va_count),
-        va_sym))
-      ++va_count;
-
-    for( ; it1!=arguments.end(); it1++, va_count++)
+    for(; it1 != arguments.end(); it1++)
     {
-      irep_idt id=
-        id2string(function_identifier)+"::va_arg"+std::to_string(va_count);
-
-      // add to symbol table
-      symbolt symbol;
-      symbol.name=id;
-      symbol.base_name="va_arg"+std::to_string(va_count);
-      symbol.mode=ID_C;
-      symbol.type=it1->type();
-
-      state.symbol_table.insert(std::move(symbol));
-
-      symbol_exprt lhs=symbol_exprt(id, it1->type());
-
-      symex_assign(state, code_assignt(lhs, *it1));
+      symbolt &va_arg = get_fresh_aux_symbol(
+        it1->type(),
+        id2string(function_identifier),
+        "va_arg",
+        state.source.pc->source_location,
+        ns.lookup(function_identifier).mode,
+        state.symbol_table);
+      va_arg.is_parameter = true;
+
+      state.call_stack().top().parameter_names.push_back(va_arg.name);
+
+      symex_assign(state, code_assignt{va_arg.symbol_expr(), *it1});
     }
   }
   else if(it1!=arguments.end())
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index d32ee5924dd..3021255fe9d 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -254,11 +254,10 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     if(op_type.id()==ID_pointer)
       return convert_bv(op);
     else if(
-      op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
-      op_type.id() == ID_bool || op_type.id() == ID_c_enum ||
-      op_type.id() == ID_c_enum_tag || op_type.id() == ID_bv)
+      can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
+      op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
-      // Cast from integer to pointer.
+      // Cast from a bitvector type to pointer.
       // We just do a zero extension.
 
       const bvt &op_bv=convert_bv(op);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 83f6bf24c27..61b3eb642d4 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -829,6 +829,10 @@ std::string smt2_convt::type2id(const typet &type) const
   {
     return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
   }
+  else if(type.id() == ID_pointer)
+  {
+    return "p" + std::to_string(to_pointer_type(type).get_width());
+  }
   else
   {
     UNREACHABLE;
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 647d50cbdbe..b7b369e25c9 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -303,8 +303,7 @@ IREP_ID_ONE(alignof)
 IREP_ID_ONE(clang_builtin_convertvector)
 IREP_ID_ONE(gcc_builtin_va_arg)
 IREP_ID_ONE(gcc_builtin_types_compatible_p)
-IREP_ID_ONE(gcc_builtin_va_arg_next)
-IREP_ID_ONE(gcc_builtin_va_list)
+IREP_ID_ONE(va_start)
 IREP_ID_ONE(gcc_float16)
 IREP_ID_ONE(gcc_float32)
 IREP_ID_ONE(gcc_float32x)