typedef unsigned long long pan_unit64_t;

void f () 
{
  /*@unused@*/ unsigned long long put = 0xFFFFFULL;
  /*@unused@*/ pan_unit64_t pt = 0xFFFFFFFFFFFFFULL;
}