1094   fiat_p256_uint1 x655;  in fiat_p256_mul()  local
1095   fiat_p256_subborrowx_u32(&x654, &x655, x653, x637, 0x0);  in fiat_p256_mul()
1097   fiat_p256_cmovznz_u32(&x656, x655, x638, x621);  in fiat_p256_mul()
1099   fiat_p256_cmovznz_u32(&x657, x655, x640, x623);  in fiat_p256_mul()
1101   fiat_p256_cmovznz_u32(&x658, x655, x642, x625);  in fiat_p256_mul()
1103   fiat_p256_cmovznz_u32(&x659, x655, x644, x627);  in fiat_p256_mul()
1105   fiat_p256_cmovznz_u32(&x660, x655, x646, x629);  in fiat_p256_mul()
1107   fiat_p256_cmovznz_u32(&x661, x655, x648, x631);  in fiat_p256_mul()
1109   fiat_p256_cmovznz_u32(&x662, x655, x650, x633);  in fiat_p256_mul()
1111   fiat_p256_cmovznz_u32(&x663, x655, x652, x635);  in fiat_p256_mul()
2101   fiat_p256_uint1 x655;  in fiat_p256_square()  local
2102   fiat_p256_subborrowx_u32(&x654, &x655, x653, x637, 0x0);  in fiat_p256_square()
2104   fiat_p256_cmovznz_u32(&x656, x655, x638, x621);  in fiat_p256_square()
2106   fiat_p256_cmovznz_u32(&x657, x655, x640, x623);  in fiat_p256_square()
2108   fiat_p256_cmovznz_u32(&x658, x655, x642, x625);  in fiat_p256_square()
2110   fiat_p256_cmovznz_u32(&x659, x655, x644, x627);  in fiat_p256_square()
2112   fiat_p256_cmovznz_u32(&x660, x655, x646, x629);  in fiat_p256_square()
2114   fiat_p256_cmovznz_u32(&x661, x655, x648, x631);  in fiat_p256_square()
2116   fiat_p256_cmovznz_u32(&x662, x655, x650, x633);  in fiat_p256_square()
2118   fiat_p256_cmovznz_u32(&x663, x655, x652, x635);  in fiat_p256_square()