$input int NCPU;
$input int NCPU_BOUND;

$input int NGPU;
$input int NGPU_BOUND;

$assume 0 < NCPU && NCPU <= NCPU_BOUND;
$assume 0 < NGPU && NCPU <= NGPU_BOUND;


int clgetDeviceIds(  cl_device_id *devices,
  cl_uint *num_devices){
  
  if(type == CPU)
  {
  while(i < num_devices){
    *(devices+i) = i;
    i++;
    if(i == NCPU)
      break;
  }
  }else{
  while(i < num_devices){
    *(devices+i) = i;
    i++;
    if(i == NGPU)
      break;
  }
  }
  }
  
  struct cl_device_id{
  device_t type;
  int id;
  }
  
  civl verify -inputNCPU_BOUND=4  -inputNGPU_BOUND=3....