37   uint64_t b0 = b[0U];  in Hacl_Bignum_Modulo_carry_top()  local
39   uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U);  in Hacl_Bignum_Modulo_carry_top()
89   uint64_t b0;  in Hacl_Bignum_Fmul_shift_reduce()  local
100   b0 = output[0U];  in Hacl_Bignum_Fmul_shift_reduce()
101   output[0U] = (uint64_t)19U * b0;  in Hacl_Bignum_Fmul_shift_reduce()
141       FStar_UInt128_uint128 b0;  in Hacl_Bignum_Fmul_fmul()  local
151       b0 = t[0U];  in Hacl_Bignum_Fmul_fmul()
154         FStar_UInt128_add(b0,  in Hacl_Bignum_Fmul_fmul()
217   FStar_UInt128_uint128 b0;  in Hacl_Bignum_Fsquare_fsquare_()  local
227   b0 = tmp[0U];  in Hacl_Bignum_Fsquare_fsquare_()
230     FStar_UInt128_add(b0,  in Hacl_Bignum_Fsquare_fsquare_()
292   uint64_t *b0 = buf + (uint32_t)10U;  in Hacl_Bignum_Crecip_crecip()  local
302   Hacl_Bignum_Fmul_fmul(b0, t00, z);  in Hacl_Bignum_Crecip_crecip()
303   Hacl_Bignum_Fmul_fmul(a0, b0, a0);  in Hacl_Bignum_Crecip_crecip()
305   Hacl_Bignum_Fmul_fmul(b0, t00, b0);  in Hacl_Bignum_Crecip_crecip()
306   Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U);  in Hacl_Bignum_Crecip_crecip()
345   uint64_t b0;  in Hacl_Bignum_fdifference()  local
351   b0 = tmp[0U];  in Hacl_Bignum_fdifference()
356   tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;  in Hacl_Bignum_fdifference()
384       FStar_UInt128_uint128 b0;  in Hacl_Bignum_fscalar()  local
397       b0 = tmp[0U];  in Hacl_Bignum_fscalar()
400         FStar_UInt128_add(b0,  in Hacl_Bignum_fscalar()
585   uint8_t *b0 = output;  in Hacl_EC_Format_fcontract_store()  local
589   store64_le(b0, o0);  in Hacl_EC_Format_fcontract_store()