193   uint64_t x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
202   uint64_t x12 = ((uint64_t)(arg1[8]) * ((arg2[7]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
208   uint64_t x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
209   uint64_t x19 = ((uint64_t)(arg1[7]) * ((arg2[8]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
210   uint64_t x20 = ((uint64_t)(arg1[7]) * ((arg2[7]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
211   uint64_t x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
212   uint64_t x22 = ((uint64_t)(arg1[7]) * ((arg2[5]) * ((uint32_t)0x2 * 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()
214   uint64_t x24 = ((uint64_t)(arg1[7]) * ((arg2[3]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
217   uint64_t x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
223   uint64_t x33 = ((uint64_t)(arg1[5]) * ((arg2[7]) * ((uint32_t)0x2 * 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()
232   uint64_t x42 = ((uint64_t)(arg1[3]) * ((arg2[7]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
239   uint64_t x49 = ((uint64_t)(arg1[7]) * (arg2[2]));  in fiat_25519_carry_mul()
240   uint64_t x50 = ((uint64_t)(arg1[7]) * ((arg2[1]) * (uint32_t)0x2));  in fiat_25519_carry_mul()
241   uint64_t x51 = ((uint64_t)(arg1[7]) * (arg2[0]));  in fiat_25519_carry_mul()
264   uint64_t x74 = ((uint64_t)(arg1[2]) * (arg2[7]));  in fiat_25519_carry_mul()
273   uint64_t x83 = ((uint64_t)(arg1[1]) * ((arg2[7]) * (uint32_t)0x2));  in fiat_25519_carry_mul()
283   uint64_t x93 = ((uint64_t)(arg1[0]) * (arg2[7]));  in fiat_25519_carry_mul()
345   out1[7] = x133;  in fiat_25519_carry_mul()
363   uint32_t x7 = ((arg1[7]) * (uint32_t)UINT8_C(0x13));  in fiat_25519_carry_square()
365   uint32_t x9 = ((arg1[7]) * (uint32_t)0x2);  in fiat_25519_carry_square()
378   uint64_t x22 = ((arg1[7]) * (x2 * (uint64_t)0x2));  in fiat_25519_carry_square()
379   uint64_t x23 = ((arg1[7]) * x5);  in fiat_25519_carry_square()
380   uint64_t x24 = ((uint64_t)(arg1[7]) * (x7 * (uint32_t)0x2));  in fiat_25519_carry_square()
484   out1[7] = x106;  in fiat_25519_carry_square()
503   uint32_t x8 = ((x7 >> 26) + (arg1[7]));  in fiat_25519_carry()
525   out1[7] = x20;  in fiat_25519_carry()
545   uint32_t x8 = ((arg1[7]) + (arg2[7]));  in fiat_25519_add()
555   out1[7] = x8;  in fiat_25519_add()
575   uint32_t x8 = ((UINT32_C(0x3fffffe) + (arg1[7])) - (arg2[7]));  in fiat_25519_sub()
585   out1[7] = x8;  in fiat_25519_sub()
604   uint32_t x8 = (UINT32_C(0x3fffffe) - (arg1[7]));  in fiat_25519_opp()
614   out1[7] = x8;  in fiat_25519_opp()
649   fiat_25519_subborrowx_u25(&x15, &x16, x14, (arg1[7]), UINT32_C(0x1ffffff));  in fiat_25519_to_bytes()
772   out1[7] = x67;  in fiat_25519_to_bytes()
817   uint32_t x12 = ((uint32_t)(arg1[20]) << 7);  in fiat_25519_from_bytes()
830   uint32_t x25 = ((uint32_t)(arg1[7]) << 5);  in fiat_25519_from_bytes()
880   out1[7] = x63;  in fiat_25519_from_bytes()