diff --git a/regression/cbmc/va_list4/main.c b/regression/cbmc/va_list4/main.c
new file mode 100644
index 0000000000..93f7426d42
--- /dev/null
+++ b/regression/cbmc/va_list4/main.c
@@ -0,0 +1,47 @@
+#ifdef __GNUC__
+
+struct __va_list_tag;
+typedef struct __va_list_tag __va_list_tag;
+typedef __builtin_va_list __gnuc_va_list[1U];
+typedef __gnuc_va_list va_list[1U];
+
+void foo(int n, ...);
+
+int main()
+{
+  foo(1, 1u);
+  foo(2, 2l);
+  foo(3, 3.0);
+  return 0;
+}
+
+void foo(int n, ...)
+{
+  va_list args;
+  __builtin_va_start((__va_list_tag *)(&args), n);
+
+  switch(n)
+  {
+  case 1:
+    __CPROVER_assert(__builtin_va_arg(&args, unsigned) == 1, "1");
+    break;
+  case 2:
+    __CPROVER_assert(__builtin_va_arg(&args, long) == 2, "2");
+    break;
+  case 3:
+    __CPROVER_assert(__builtin_va_arg(&args, double) == 3.0, "3");
+    break;
+  }
+
+  __builtin_va_end((__va_list_tag *)(&args));
+}
+
+#else
+
+// __builtin_va_list is GCC/Clang-only
+
+int main()
+{
+}
+
+#endif
diff --git a/regression/cbmc/va_list4/test.desc b/regression/cbmc/va_list4/test.desc
new file mode 100644
index 0000000000..9efefbc736
--- /dev/null
+++ b/regression/cbmc/va_list4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 3288690ab5..986f32aa58 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -602,19 +602,23 @@ void goto_convertt::do_array_op(
 
 exprt make_va_list(const exprt &expr)
 {
-  // we first strip any typecast
-  if(expr.id()==ID_typecast)
-    return make_va_list(to_typecast_expr(expr).op());
+  exprt result = skip_typecast(expr);
 
   // if it's an address of an lvalue, we take that
-  if(expr.id() == ID_address_of)
+  if(result.id() == ID_address_of)
   {
-    const auto &address_of_expr = to_address_of_expr(expr);
+    const auto &address_of_expr = to_address_of_expr(result);
     if(is_lvalue(address_of_expr.object()))
-      return address_of_expr.object();
+      result = address_of_expr.object();
   }
 
-  return expr;
+  while(result.type().id() == ID_array &&
+        to_array_type(result.type()).size().is_one())
+  {
+    result = index_exprt{result, from_integer(0, index_type())};
+  }
+
+  return result;
 }
 
 /// add function calls to function queue for later processing