fix index out of bounds error of x86_64 ABI

This fixes #5754.