23 // t[3]+2^102 t[4]+...+2^230 t[9].
196   uint64_t x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
205   uint64_t x15 = ((uint64_t)(arg1[8]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
213   uint64_t x23 = ((uint64_t)(arg1[7]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
220   uint64_t x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
226   uint64_t x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
227   uint64_t x37 = ((uint64_t)(arg1[4]) * ((arg2[8]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
228   uint64_t x38 = ((uint64_t)(arg1[4]) * ((arg2[7]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
229   uint64_t x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
246   uint64_t x56 = ((uint64_t)(arg1[5]) * (arg2[4]));  in fiat_25519_carry_mul()
251   uint64_t x61 = ((uint64_t)(arg1[4]) * (arg2[5]));  in fiat_25519_carry_mul()
252   uint64_t x62 = ((uint64_t)(arg1[4]) * (arg2[4]));  in fiat_25519_carry_mul()
253   uint64_t x63 = ((uint64_t)(arg1[4]) * (arg2[3]));  in fiat_25519_carry_mul()
254   uint64_t x64 = ((uint64_t)(arg1[4]) * (arg2[2]));  in fiat_25519_carry_mul()
255   uint64_t x65 = ((uint64_t)(arg1[4]) * (arg2[1]));  in fiat_25519_carry_mul()
256   uint64_t x66 = ((uint64_t)(arg1[4]) * (arg2[0]));  in fiat_25519_carry_mul()
259   uint64_t x69 = ((uint64_t)(arg1[3]) * (arg2[4]));  in fiat_25519_carry_mul()
267   uint64_t x77 = ((uint64_t)(arg1[2]) * (arg2[4]));  in fiat_25519_carry_mul()
276   uint64_t x86 = ((uint64_t)(arg1[1]) * (arg2[4]));  in fiat_25519_carry_mul()
286   uint64_t x96 = ((uint64_t)(arg1[0]) * (arg2[4]));  in fiat_25519_carry_mul()
342   out1[4] = x124;  in fiat_25519_carry_mul()
371   uint32_t x15 = ((arg1[4]) * (uint32_t)0x2);  in fiat_25519_carry_square()
390   uint64_t x34 = ((uint64_t)(arg1[4]) * x2);  in fiat_25519_carry_square()
391   uint64_t x35 = ((arg1[4]) * x5);  in fiat_25519_carry_square()
392   uint64_t x36 = ((uint64_t)(arg1[4]) * x8);  in fiat_25519_carry_square()
393   uint64_t x37 = ((arg1[4]) * x11);  in fiat_25519_carry_square()
394   uint64_t x38 = ((uint64_t)(arg1[4]) * x14);  in fiat_25519_carry_square()
395   uint64_t x39 = ((uint64_t)(arg1[4]) * (arg1[4]));  in fiat_25519_carry_square()
481   out1[4] = x97;  in fiat_25519_carry_square()
500   uint32_t x5 = ((x4 >> 25) + (arg1[4]));  in fiat_25519_carry()
522   out1[4] = x17;  in fiat_25519_carry()
542   uint32_t x5 = ((arg1[4]) + (arg2[4]));  in fiat_25519_add()
552   out1[4] = x5;  in fiat_25519_add()
572   uint32_t x5 = ((UINT32_C(0x7fffffe) + (arg1[4])) - (arg2[4]));  in fiat_25519_sub()
582   out1[4] = x5;  in fiat_25519_sub()
601   uint32_t x5 = (UINT32_C(0x7fffffe) - (arg1[4]));  in fiat_25519_opp()
611   out1[4] = x5;  in fiat_25519_opp()
640   fiat_25519_subborrowx_u26(&x9, &x10, x8, (arg1[4]), UINT32_C(0x3ffffff));  in fiat_25519_to_bytes()
689   uint32_t x43 = (x38 << 4);  in fiat_25519_to_bytes()
769   out1[4] = x60;  in fiat_25519_to_bytes()
811   uint32_t x6 = ((uint32_t)(arg1[26]) << 4);  in fiat_25519_from_bytes()
833   uint32_t x28 = ((uint32_t)(arg1[4]) << 6);  in fiat_25519_from_bytes()
877   out1[4] = x55;  in fiat_25519_from_bytes()