Incorrect value from __builtin_va_arg on a va_list element pointer passed to a function

[71iq]

Version

CBMC version: 6.10.0 (cbmc-6.10.0-29-g357954eca6, develop build)
Operating system: Linux x86_64
Reference compiler: GCC 14.3.0

Code to reproduce

#include <assert.h>

typedef typeof(((__builtin_va_list *)0)[0][0]) va_tag;

void read_arg(va_tag *args)
{
  assert(__builtin_va_arg(args, int) == 5);
}

void foo(int first, ...)
{
  va_tag args[1];
  __builtin_va_start(args, first);
  read_arg(args);
  __builtin_va_end(args);
}

int main(void)
{
  foo(0, 5);
}

Commands:

gcc -std=gnu11 -Wall -Wextra va_arg_repro.c -o repro && ./repro
cbmc va_arg_repro.c --trace

Behavior

I expect the assertion to pass: the first variadic argument is the int
value 5. On GCC x86_64, __builtin_va_list is a one-element array;
va_tag extracts its element type, and va_tag args[1] reconstructs
that representation. Passing args to read_arg produces a pointer to
the element. GCC compiles this without warnings and the executable exits
with status 0.

What happened instead was:

[read_arg.assertion.1] line 7 assertion __builtin_va_arg(args, int) == 5: FAILURE

** 1 of 13 failed (2 iterations)
VERIFICATION FAILED

CBMC exits with status 10. All twelve generated pointer-dereference checks
pass, but the trace shows return_value_gcc_builtin_va_arg=0 instead of 5.