Lines Matching refs:b4
1131 + FStar_UInt128_t b4;
1148 - FStar_UInt128_t b4 = t[4U];
1151 - b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)…
1155 + b4 = t[4U];
1157 + b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
1160 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1218 + FStar_UInt128_t b4;
1228 - FStar_UInt128_t b4 = tmp[4U];
1231 - b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)…
1234 + b4 = tmp[4U];
1236 + b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
1240 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1341 + uint64_t b4;
1347 - uint64_t b4 = tmp[4U];
1352 + b4 = tmp[4U];
1364 + FStar_UInt128_t b4;
1377 - FStar_UInt128_t b4 = tmp[4U];
1380 - b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)…
1383 + b4 = tmp[4U];
1385 + b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
1389 … FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
1675 + uint32_t b4;
1682 - uint32_t b4 = tmp[4U];
1683 - uint32_t b4_ = (uint32_t)0x1000000U | b4;
1684 + b4 = tmp[4U];
1685 + b4_ = (uint32_t)0x1000000U | b4;