1  /* { dg-do run } */
       2  /* { dg-require-effective-target stdint_types } */
       3  /* { dg-options "-O2 -Wno-psabi -w" } */
       4  /* { dg-additional-options "-mno-sse2" { target x86_64-*-* i?86-*-* } } */
       5  
       6  #include <stdint.h>
       7  
       8  typedef uint8_t u8;
       9  typedef uint16_t u16;
      10  typedef uint32_t u32;
      11  typedef uint64_t u64;
      12  typedef u64 __attribute__((__vector_size__ (16))) v128u64;
      13  u16 foo0_u16_0;
      14  v128u64 foo0_v64u32_0;
      15  u64 foo0_u64_0;
      16  v128u64 foo0_v128u64_2;
      17  
      18  v128u64
      19  foo0 (u8 u8_0, v128u64 v128u64_0)
      20  {
      21    u32 u32_1 = u8_0 || (0, 0);
      22    foo0_v128u64_2 - u8_0;
      23    foo0_u16_0 |= foo0_u64_0 && u8_0 > foo0_u64_0 <= u32_1;
      24    v128u64 v128u64_4 = v128u64_0 >= u8_0;
      25    return v128u64_4 + foo0_v64u32_0;
      26  }
      27  
      28  int
      29  main ()
      30  {
      31    v128u64 x = foo0 (3, (v128u64) { 0, 12 });
      32    if (x[0] != 0) __builtin_abort();
      33    if (x[1] != 0xffffffffffffffff) __builtin_abort();
      34    return 0;
      35  }