#include <stdint.h>
uint64_t cmovznz(uint64_t t, uint64_t z, uint64_t nz);
uint64_t cmovznz64(uint64_t t, uint64_t z, uint64_t nz);