#include <stdint.h>

void inc128big(int8_t x[16])
{
  for (int i = 15;i >= 0;--i)
    if (++x[i])
      break;
}