check_args
/* Autogenerated: '../src/ExtractionOCaml/unsaturated_solinas' --no-primitives --no-wide-int --shiftr-avoid-uint1 --output '/dev/null' --output-asm '/dev/null' --tight-bounds-mul-by 1.000001 curve25519 64 5 '2^255 - 19' carry_square --hints-file './9789_ratio10114_seed1785685356_square_curve25519.asm' */
/* curve description: curve25519 */
/* machine_wordsize = 64 (from "64") */
/* requested operations: carry_square */
/* n = 5 (from "5") */
/* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */
/* tight_bounds_multiplier = 1.000001 (from "1.000001") */
/*  */
/* Computed values: */
/*   carry_chain = [0, 1, 2, 3, 4, 0, 1] */
/*   eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204) */
/*   bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
/*   balance = [0xfffffffffffda, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */

#include <stdint.h>
#ifdef __GNUC__
#  define FIAT_CURVE25519_FIAT_INLINE __inline__
#else
#  define FIAT_CURVE25519_FIAT_INLINE
#endif

#if (-1 & 3) != 3
#error "This code only works on a two's complement system"
#endif



In fiat_curve25519_carry_square:
Error while checking for equivalence of syntax tree and assembly:
The syntax tree:
(λ x1,
  let x2 := x1[4] * 19 (* : uint64_t *) in
  let x3 := x2 * 2 (* : uint64_t *) in
  let x4 := x1[4] * 2 (* : uint64_t *) in
  let x5 := x1[3] * 19 (* : uint64_t *) in
  let x6 := x5 * 2 (* : uint64_t *) in
  let x7 := x1[3] * 2 (* : uint64_t *) in
  let x8 := x1[2] * 2 (* : uint64_t *) in
  let x9 := x1[1] * 2 (* : uint64_t *) in
  let x10 := Z.mul_split(2^64, None, (x1[4], Some [0x0 ~> 0xffffffffffffffff], (x2, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x11 := Z.mul_split(2^64, None, (x1[3], Some [0x0 ~> 0xffffffffffffffff], (x3, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x12 := Z.mul_split(2^64, None, (x1[3], Some [0x0 ~> 0xffffffffffffffff], (x5, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x13 := Z.mul_split(2^64, None, (x1[2], Some [0x0 ~> 0xffffffffffffffff], (x3, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x14 := Z.mul_split(2^64, None, (x1[2], Some [0x0 ~> 0xffffffffffffffff], (x6, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x15 := Z.mul_split(2^64, None, (x1[2], Some [0x0 ~> 0xffffffffffffffff], (x1[2], Some [0x0 ~> 0xffffffffffffffff]))) in
  let x16 := Z.mul_split(2^64, None, (x1[1], Some [0x0 ~> 0xffffffffffffffff], (x3, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x17 := Z.mul_split(2^64, None, (x1[1], Some [0x0 ~> 0xffffffffffffffff], (x7, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x18 := Z.mul_split(2^64, None, (x1[1], Some [0x0 ~> 0xffffffffffffffff], (x8, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x19 := Z.mul_split(2^64, None, (x1[1], Some [0x0 ~> 0xffffffffffffffff], (x1[1], Some [0x0 ~> 0xffffffffffffffff]))) in
  let x20 := Z.mul_split(2^64, None, (x1[0], Some [0x0 ~> 0xffffffffffffffff], (x4, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x21 := Z.mul_split(2^64, None, (x1[0], Some [0x0 ~> 0xffffffffffffffff], (x7, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x22 := Z.mul_split(2^64, None, (x1[0], Some [0x0 ~> 0xffffffffffffffff], (x8, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x23 := Z.mul_split(2^64, None, (x1[0], Some [0x0 ~> 0xffffffffffffffff], (x9, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x24 := Z.mul_split(2^64, None, (x1[0], Some [0x0 ~> 0xffffffffffffffff], (x1[0], Some [0x0 ~> 0xffffffffffffffff]))) in
  let x25 := Z.add_get_carry(2^64, None, (x16₁, Some [0x0 ~> 0xffffffffffffffff], (x14₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x26 := Z.add_with_get_carry(2^64, None, (x25₂, Some [0x0 ~> 0x1], (x16₂, Some [0x0 ~> 0xffffffffffffffff], (x14₂, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x27 := Z.add_get_carry(2^64, None, (x24₁, Some [0x0 ~> 0xffffffffffffffff], (x25₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x28 := Z.add_with_get_carry(2^64, None, (x27₂, Some [0x0 ~> 0x1], (x24₂, Some [0x0 ~> 0xffffffffffffffff], (x26₁, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x29 := (x27₁ >> 51) | Z.truncating_shiftl(64, None, (x28₁, Some [0x0 ~> 0xffffffffffffffff], (13, None))) (* : uint64_t *) in
  let x30 := x27₁ & (2^51-1) (* : uint64_t *) in
  let x31 := Z.add_get_carry(2^64, None, (x17₁, Some [0x0 ~> 0xffffffffffffffff], (x15₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x32 := Z.add_with_get_carry(2^64, None, (x31₂, Some [0x0 ~> 0x1], (x17₂, Some [0x0 ~> 0xffffffffffffffff], (x15₂, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x33 := Z.add_get_carry(2^64, None, (x20₁, Some [0x0 ~> 0xffffffffffffffff], (x31₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x34 := Z.add_with_get_carry(2^64, None, (x33₂, Some [0x0 ~> 0x1], (x20₂, Some [0x0 ~> 0xffffffffffffffff], (x32₁, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x35 := Z.add_get_carry(2^64, None, (x18₁, Some [0x0 ~> 0xffffffffffffffff], (x10₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x36 := Z.add_with_get_carry(2^64, None, (x35₂, Some [0x0 ~> 0x1], (x18₂, Some [0x0 ~> 0xffffffffffffffff], (x10₂, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x37 := Z.add_get_carry(2^64, None, (x21₁, Some [0x0 ~> 0xffffffffffffffff], (x35₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x38 := Z.add_with_get_carry(2^64, None, (x37₂, Some [0x0 ~> 0x1], (x21₂, Some [0x0 ~> 0xffffffffffffffff], (x36₁, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x39 := Z.add_get_carry(2^64, None, (x19₁, Some [0x0 ~> 0xffffffffffffffff], (x11₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x40 := Z.add_with_get_carry(2^64, None, (x39₂, Some [0x0 ~> 0x1], (x19₂, Some [0x0 ~> 0xffffffffffffffff], (x11₂, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x41 := Z.add_get_carry(2^64, None, (x22₁, Some [0x0 ~> 0xffffffffffffffff], (x39₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x42 := Z.add_with_get_carry(2^64, None, (x41₂, Some [0x0 ~> 0x1], (x22₂, Some [0x0 ~> 0xffffffffffffffff], (x40₁, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x43 := Z.add_get_carry(2^64, None, (x13₁, Some [0x0 ~> 0xffffffffffffffff], (x12₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x44 := Z.add_with_get_carry(2^64, None, (x43₂, Some [0x0 ~> 0x1], (x13₂, Some [0x0 ~> 0xffffffffffffffff], (x12₂, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x45 := Z.add_get_carry(2^64, None, (x23₁, Some [0x0 ~> 0xffffffffffffffff], (x43₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x46 := Z.add_with_get_carry(2^64, None, (x45₂, Some [0x0 ~> 0x1], (x23₂, Some [0x0 ~> 0xffffffffffffffff], (x44₁, Some [0x0 ~> 0xffffffffffffffff])))) in
  let x47 := Z.add_get_carry(2^64, None, (x29, Some [0x0 ~> 0xffffffffffffffff], (x45₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x48 := x47₂ + x46₁ (* : uint64_t *) in
  let x49 := (x47₁ >> 51) | Z.truncating_shiftl(64, None, (x48, Some [0x0 ~> 0xffffffffffffffff], (13, None))) (* : uint64_t *) in
  let x50 := x47₁ & (2^51-1) (* : uint64_t *) in
  let x51 := Z.add_get_carry(2^64, None, (x49, Some [0x0 ~> 0xffffffffffffffff], (x41₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x52 := x51₂ + x42₁ (* : uint64_t *) in
  let x53 := (x51₁ >> 51) | Z.truncating_shiftl(64, None, (x52, Some [0x0 ~> 0xffffffffffffffff], (13, None))) (* : uint64_t *) in
  let x54 := x51₁ & (2^51-1) (* : uint64_t *) in
  let x55 := Z.add_get_carry(2^64, None, (x53, Some [0x0 ~> 0xffffffffffffffff], (x37₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x56 := x55₂ + x38₁ (* : uint64_t *) in
  let x57 := (x55₁ >> 51) | Z.truncating_shiftl(64, None, (x56, Some [0x0 ~> 0xffffffffffffffff], (13, None))) (* : uint64_t *) in
  let x58 := x55₁ & (2^51-1) (* : uint64_t *) in
  let x59 := Z.add_get_carry(2^64, None, (x57, Some [0x0 ~> 0xffffffffffffffff], (x33₁, Some [0x0 ~> 0xffffffffffffffff]))) in
  let x60 := x59₂ + x34₁ (* : uint64_t *) in
  let x61 := (x59₁ >> 51) | Z.truncating_shiftl(64, None, (x60, Some [0x0 ~> 0xffffffffffffffff], (13, None))) (* : uint64_t *) in
  let x62 := x59₁ & (2^51-1) (* : uint64_t *) in
  let x63 := x61 * 19 (* : uint64_t *) in
  let x64 := x30 + x63 (* : uint64_t *) in
  let x65 := x64 >> 51 (* : uint64_t *) in
  let x66 := x64 & (2^51-1) (* : uint64_t *) in
  let x67 := x65 + x50 (* : uint64_t *) in
  let x68 := x67 >> 51 (* : uint64_t *) in
  let x69 := x67 & (2^51-1) (* : uint64_t *) in
  let x70 := x68 + x54 (* : uint64_t *) in
  x66 :: x69 :: x70 :: x58 :: x62 :: []
)

which can be pretty-printed as:
/*
 * Input Bounds:
 *   arg1: [[0x0 ~> 0x18000192a73712], [0x0 ~> 0x18000192a73712], [0x0 ~> 0x18000192a73712], [0x0 ~> 0x18000192a73712], [0x0 ~> 0x18000192a73712]]
 * Output Bounds:
 *   out1: None
 */
void f(uint64_t out1[5], const uint64_t arg1[5]) {
  uint64_t x1;
  uint64_t x2;
  uint64_t x3;
  uint64_t x4;
  uint64_t x5;
  uint64_t x6;
  uint64_t x7;
  uint64_t x8;
  uint64_t x9;
  uint64_t x10;
  uint64_t x11;
  uint64_t x12;
  uint64_t x13;
  uint64_t x14;
  uint64_t x15;
  uint64_t x16;
  uint64_t x17;
  uint64_t x18;
  uint64_t x19;
  uint64_t x20;
  uint64_t x21;
  uint64_t x22;
  uint64_t x23;
  uint64_t x24;
  uint64_t x25;
  uint64_t x26;
  uint64_t x27;
  uint64_t x28;
  uint64_t x29;
  uint64_t x30;
  uint64_t x31;
  uint64_t x32;
  uint64_t x33;
  uint64_t x34;
  uint64_t x35;
  uint64_t x36;
  uint64_t x37;
  uint64_t x38;
  uint64_t x39;
  uint1 x40;
  uint64_t x41;
  uint1 x42;
  uint64_t x43;
  uint1 x44;
  uint64_t x45;
  uint1 x46;
  uint64_t x47;
  uint64_t x48;
  uint64_t x49;
  uint1 x50;
  uint64_t x51;
  uint1 x52;
  uint64_t x53;
  uint1 x54;
  uint64_t x55;
  uint1 x56;
  uint64_t x57;
  uint1 x58;
  uint64_t x59;
  uint1 x60;
  uint64_t x61;
  uint1 x62;
  uint64_t x63;
  uint1 x64;
  uint64_t x65;
  uint1 x66;
  uint64_t x67;
  uint1 x68;
  uint64_t x69;
  uint1 x70;
  uint64_t x71;
  uint1 x72;
  uint64_t x73;
  uint1 x74;
  uint64_t x75;
  uint1 x76;
  uint64_t x77;
  uint1 x78;
  uint64_t x79;
  uint1 x80;
  uint64_t x81;
  uint1 x82;
  uint64_t x83;
  uint64_t x84;
  uint64_t x85;
  uint64_t x86;
  uint1 x87;
  uint64_t x88;
  uint64_t x89;
  uint64_t x90;
  uint64_t x91;
  uint1 x92;
  uint64_t x93;
  uint64_t x94;
  uint64_t x95;
  uint64_t x96;
  uint1 x97;
  uint64_t x98;
  uint64_t x99;
  uint64_t x100;
  uint64_t x101;
  uint64_t x102;
  uint64_t x103;
  uint64_t x104;
  uint64_t x105;
  uint64_t x106;
  uint64_t x107;
  uint64_t x108;
  x1 = ((arg1[4]) * (uint64_t)UINT8_C(0x13));
  x2 = (x1 * (uint64_t)0x2);
  x3 = ((arg1[4]) * (uint64_t)0x2);
  x4 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
  x5 = (x4 * (uint64_t)0x2);
  x6 = ((arg1[3]) * (uint64_t)0x2);
  x7 = ((arg1[2]) * (uint64_t)0x2);
  x8 = ((arg1[1]) * (uint64_t)0x2);
  mulx_u64(&x9, &x10, (arg1[4]), x1);
  mulx_u64(&x11, &x12, (arg1[3]), x2);
  mulx_u64(&x13, &x14, (arg1[3]), x4);
  mulx_u64(&x15, &x16, (arg1[2]), x2);
  mulx_u64(&x17, &x18, (arg1[2]), x5);
  mulx_u64(&x19, &x20, (arg1[2]), (arg1[2]));
  mulx_u64(&x21, &x22, (arg1[1]), x2);
  mulx_u64(&x23, &x24, (arg1[1]), x6);
  mulx_u64(&x25, &x26, (arg1[1]), x7);
  mulx_u64(&x27, &x28, (arg1[1]), (arg1[1]));
  mulx_u64(&x29, &x30, (arg1[0]), x3);
  mulx_u64(&x31, &x32, (arg1[0]), x6);
  mulx_u64(&x33, &x34, (arg1[0]), x7);
  mulx_u64(&x35, &x36, (arg1[0]), x8);
  mulx_u64(&x37, &x38, (arg1[0]), (arg1[0]));
  addcarryx_u64(&x39, &x40, 0x0, x21, x17);
  addcarryx_u64(&x41, &x42, x40, x22, x18);
  addcarryx_u64(&x43, &x44, 0x0, x37, x39);
  addcarryx_u64(&x45, &x46, x44, x38, x41);
  x47 = ((x43 >> 51) | ((x45 << 13) & UINT64_C(0xffffffffffffffff)));
  x48 = (x43 & UINT64_C(0x7ffffffffffff));
  addcarryx_u64(&x49, &x50, 0x0, x23, x19);
  addcarryx_u64(&x51, &x52, x50, x24, x20);
  addcarryx_u64(&x53, &x54, 0x0, x29, x49);
  addcarryx_u64(&x55, &x56, x54, x30, x51);
  addcarryx_u64(&x57, &x58, 0x0, x25, x9);
  addcarryx_u64(&x59, &x60, x58, x26, x10);
  addcarryx_u64(&x61, &x62, 0x0, x31, x57);
  addcarryx_u64(&x63, &x64, x62, x32, x59);
  addcarryx_u64(&x65, &x66, 0x0, x27, x11);
  addcarryx_u64(&x67, &x68, x66, x28, x12);
  addcarryx_u64(&x69, &x70, 0x0, x33, x65);
  addcarryx_u64(&x71, &x72, x70, x34, x67);
  addcarryx_u64(&x73, &x74, 0x0, x15, x13);
  addcarryx_u64(&x75, &x76, x74, x16, x14);
  addcarryx_u64(&x77, &x78, 0x0, x35, x73);
  addcarryx_u64(&x79, &x80, x78, x36, x75);
  addcarryx_u64(&x81, &x82, 0x0, x47, x77);
  x83 = (x82 + x79);
  x84 = ((x81 >> 51) | ((x83 << 13) & UINT64_C(0xffffffffffffffff)));
  x85 = (x81 & UINT64_C(0x7ffffffffffff));
  addcarryx_u64(&x86, &x87, 0x0, x84, x69);
  x88 = (x87 + x71);
  x89 = ((x86 >> 51) | ((x88 << 13) & UINT64_C(0xffffffffffffffff)));
  x90 = (x86 & UINT64_C(0x7ffffffffffff));
  addcarryx_u64(&x91, &x92, 0x0, x89, x61);
  x93 = (x92 + x63);
  x94 = ((x91 >> 51) | ((x93 << 13) & UINT64_C(0xffffffffffffffff)));
  x95 = (x91 & UINT64_C(0x7ffffffffffff));
  addcarryx_u64(&x96, &x97, 0x0, x94, x53);
  x98 = (x97 + x55);
  x99 = ((x96 >> 51) | ((x98 << 13) & UINT64_C(0xffffffffffffffff)));
  x100 = (x96 & UINT64_C(0x7ffffffffffff));
  x101 = (x99 * (uint64_t)UINT8_C(0x13));
  x102 = (x48 + x101);
  x103 = (x102 >> 51);
  x104 = (x102 & UINT64_C(0x7ffffffffffff));
  x105 = (x103 + x85);
  x106 = (x105 >> 51);
  x107 = (x105 & UINT64_C(0x7ffffffffffff));
  x108 = (x106 + x90);
  out1[0] = x104;
  out1[1] = x107;
  out1[2] = x108;
  out1[3] = x95;
  out1[4] = x100;
}


Assembly:
square_curve25519:
sub rsp, 152
mov rax, [rsi + 0x08 * 1]; load m64 arg1[1] to register64
mov r10, rax; load m64 x8 to register64
shl r10, 1; x8 <- arg1[1] * 0x2
imul rax, [rsi + 0x08 * 3], 38; x5 <- arg1[3] * 0x26
mov r11, [rsi + 0x08 * 2]; load m64 arg1[2] to register64
lea rdx, [r11 + 1 * r11]; x7 <- arg1[2] * 2 
mov r11, rdx; preserving value of x7 into a new reg
mov rdx, [rsi + 0x08 * 0]; saving arg1[0] in rdx.
mulx r8, rcx, rdx; x23_1, x23_0<- arg1[0]^2
mov rdx, [rsi + 0x08 * 4]; load m64 arg1[4] to register64
mov [rsp + 0x08 * 0], rbx; spilling calSv-rbx to mem

; imul rbx, rdx, 0x13

lea r9, [rdx + 8 * rdx]; TMP <- arg1[4] * 9
lea rbx, [rdx + 2 * r9]; x1 <- arg1[4]*19: arg1[4] + 2 * TMP = arg1[4] + 2 * 9 * arg1[4]

mov rdx, rbx; x1 to rdx
mulx rbx, r9, [rsi + 0x08 * 4]; x9_1, x9_0<- arg1[4] * x1 (_0*_0)
imul rdx, [rsi + 0x08 * 3], 19; x4 <- arg1[3] * 0x13
mov [rsp + 0x08 * 1], rbp; spilling calSv-rbp to mem
mov rbp, rdx; preserving value of x4 into a new reg
mov rdx, [rsi + 0x08 * 0]; saving arg1[0] in rdx.
mov [rsp + 0x08 * 2], r12; spilling calSv-r12 to mem
mov [rsp + 0x08 * 3], r13; spilling calSv-r13 to mem
mulx r13, r12, r11; x21_1, x21_0<- arg1[0] * x7 (_0*_0)
mov rdx, rbp; x4 to rdx
mov [rsp + 0x08 * 4], r14; spilling calSv-r14 to mem
mulx r14, rbp, [rsi + 0x08 * 3]; x11_1, x11_0<- arg1[3] * x4 (_0*_0)
mov rdx, [rsi + 0x08 * 1]; arg1[1] to rdx
mov [rsp + 0x08 * 5], r15; spilling calSv-r15 to mem
mov [rsp + 0x08 * 6], rdi; spilling out1 to mem
mulx rdi, r15, rdx; x18_1, x18_0<- arg1[1]^2
mov rdx, [rsi + 0x08 * 4]; load m64 arg1[4] to register64
mov [rsp + 0x08 * 7], r14; spilling x11_1 to mem
lea r14, [rdx + 1 * rdx]; x3 <- arg1[4] * 2 
mov rdx, [rsi + 0x08 * 1]; arg1[1] to rdx
mov [rsp + 0x08 * 8], rbp; spilling x11_0 to mem
mov [rsp + 0x08 * 9], r8; spilling x23_1 to mem
mulx r8, rbp, r11; x17_1, x17_0<- arg1[1] * x7 (_0*_0)
mov rdx, r10; x8 to rdx
mulx r11, r10, [rsi + 0x08 * 0]; x22_1, x22_0<- arg1[0] * x8 (_0*_0)
xor rdx, rdx
adox r9, rbp
adox r8, rbx
mov rbx, [rsi + 0x08 * 3]; load m64 arg1[3] to register64
mov rbp, rbx; load m64 x6 to register64
shl rbp, 1; x6 <- arg1[3] * 0x2
mov rdx, rbp; x6 to rdx
mulx rbp, rbx, [rsi + 0x08 * 0]; x20_1, x20_0<- arg1[0] * x6 (_0*_0)
mov [rsp + 0x08 * 10], r8; spilling x10002_1 to mem
mov r8, rdx; preserving value of x6 into a new reg
mov rdx, [rsi + 0x08 * 0]; saving arg1[0] in rdx.
mov [rsp + 0x08 * 11], r9; spilling x10002_0 to mem
mov [rsp + 0x08 * 12], rbp; spilling x20_1 to mem
mulx rbp, r9, r14; x19_1, x19_0<- arg1[0] * x3 (_0*_0)
imul rdx, [rsi + 0x08 * 4], 38; x2 <- arg1[4] * 0x26
mov [rsp + 0x08 * 13], rbx; spilling x20_0 to mem
mulx rbx, r14, [rsi + 0x08 * 3]; x10_1, x10_0<- arg1[3] * x2 (_0*_0)
mov [rsp + 0x08 * 14], r11; spilling x22_1 to mem
mov [rsp + 0x08 * 15], r10; spilling x22_0 to mem
mulx r10, r11, [rsi + 0x08 * 1]; x15_1, x15_0<- arg1[1] * x2 (_0*_0)
mov [rsp + 0x08 * 16], rcx; spilling x23_0 to mem
mov [rsp + 0x08 * 17], r10; spilling x15_1 to mem
mulx r10, rcx, [rsi + 0x08 * 2]; x12_1, x12_0<- arg1[2] * x2 (_0*_0)
test al, al
adox r14, r15
adox rdi, rbx
mov rdx, rax; x5 to rdx
mulx r15, rax, [rsi + 0x08 * 2]; x13_1, x13_0<- arg1[2] * x5 (_0*_0)
mov rdx, [rsi + 0x08 * 2]; arg1[2] to rdx
mov [rsp + 0x08 * 18], r10; spilling x12_1 to mem
mulx r10, rbx, rdx; x14_1, x14_0<- arg1[2]^2
adcx r14, r12
adcx r13, rdi
mov rdx, r8; x6 to rdx
mulx r12, r8, [rsi + 0x08 * 1]; x16_1, x16_0<- arg1[1] * x6 (_0*_0)
test al, al
adox rbx, r8
adox r12, r10
adcx rbx, r9
adcx rbp, r12
xor rdx, rdx
adox rax, r11
adox r15, [rsp + 0x08 * 17]
adcx rax, [rsp + 0x08 * 16]
adcx r15, [rsp + 0x08 * 9]
mov r9, rax;x25, copying x24_0 here, cause x24_0 is needed in a reg. It has those deps: "x25, x26, size: 2", current hard deps: ""
shrd r9, r15, 51; x25 <- x24_1||x24_0 >> 51
mov r11, rcx;x10004_0, copying x12_0 here, cause x12_0 is needed in a reg. It has those deps: "", current hard deps: "x12_0"
add r11, [rsp + 0x08 * 8]; could be done better, if r0 has been u8 as well
mov rdi, [rsp + 0x08 * 7]; load m64 x11_1 to register64
adcx rdi, [rsp + 0x08 * 18]
xor rcx, rcx
adox r11, [rsp + 0x08 * 15]
adox rdi, [rsp + 0x08 * 14]
adcx r11, r9
adc rdi, 0; add CF to r0's alloc
mov rdx, r11;x32, copying x31_0 here, cause x31_0 is needed in a reg. It has those deps: "x32, x33, size: 2", current hard deps: ""
shrd rdx, rdi, 51; x32 <- x31_1||x31_0 >> 51
test al, al
adox r14, rdx
adox r13, rcx
mov r10, [rsp + 0x08 * 11]; load m64 x10002_0 to register64
adcx r10, [rsp + 0x08 * 13]
mov r8, [rsp + 0x08 * 10]; load m64 x10002_1 to register64
adcx r8, [rsp + 0x08 * 12]
mov r12, r14;x35, copying x34_0 here, cause x34_0 is needed in a reg. It has those deps: "x35, x36, size: 2", current hard deps: ""
shrd r12, r13, 51; x35 <- x34_1||x34_0 >> 51
xor r15, r15
adox r10, r12
adox r8, r15
mov rcx, r10;x38, copying x37_0 here, cause x37_0 is needed in a reg. It has those deps: "x38, x39, size: 2", current hard deps: ""
shrd rcx, r8, 51; x38 <- x37_1||x37_0 >> 51
xor r9, r9
adox rbx, rcx
adox rbp, r9
mov r15, 51 ; moving imm to reg
bzhi rdi, r10, r15; x39 <- x37_0 (only least 0x33 bits)
mov rdx, rbx;x41, copying x40_0 here, cause x40_0 is needed in a reg. It has those deps: "x41, x42, size: 2", current hard deps: ""
shrd rdx, rbp, 51; x41 <- x40_1||x40_0 >> 51
bzhi r13, rbx, r15; x42 <- x40_0 (only least 0x33 bits)
bzhi r12, rax, r15; x26 <- x24_0 (only least 0x33 bits)
mov rax, [rsp + 0x08 * 6]; load m64 out1 to register64
mov [rax + 0x08 * 4], r13; out1[4] = x42

; using imul works
; imul r8, rdx, 0x13

; this does not.
lea r10, [rdx + 8 * rdx]; TMP <- x41 * 9
lea r8, [rdx + 2 * r10]; x43 <- x41*19: x41 + 2 * TMP = x41 + 2 * 9 * x41


lea r12, [r12 + 1 * r8]
bzhi r10, r11, r15; x33 <- x31_0 (only least 0x33 bits)
bzhi r11, r12, r15; x46 <- x44 (only least 0x33 bits)
shr r12, 51; x45 <- x44>> 51
lea r12, [r12 + 1 * r10]
mov rcx, r12;x48, copying x47 here, cause x47 is needed in a reg. It has those deps: "x48, x49, size: 2", current hard deps: ""
shr rcx, 51; x48 <- x47>> 51
bzhi rbx, r14, r15; x36 <- x34_0 (only least 0x33 bits)
mov [rax + 0x08 * 0], r11; out1[0] = x46
lea rcx, [rcx + 1 * rbx]
mov [rax + 0x08 * 2], rcx; out1[2] = x50
bzhi r14, r12, r15; x49 <- x47 (only least 0x33 bits)
mov [rax + 0x08 * 3], rdi; out1[3] = x39
mov [rax + 0x08 * 1], r14; out1[1] = x49
mov rbx, [rsp + 0x08 * 0] ; pop
mov rbp, [rsp + 0x08 * 1] ; pop
mov r12, [rsp + 0x08 * 2] ; pop
mov r13, [rsp + 0x08 * 3] ; pop
mov r14, [rsp + 0x08 * 4] ; pop
mov r15, [rsp + 0x08 * 5] ; pop
add rsp, 152
ret
; cpu Intel(R) Core(TM) i5-8265U CPU @ 1.60GHz
; ratio 1.0114
; seed 1785685356 
; CC / CFLAGS clang / -march=native -mtune=native -O3 
; time needed: 1758 ms / 100 evals=> 17.58ms/eval
; Time spent for assembling and measureing (initial batch_size=161, initial num_batches=31): 101 ms
; number of used evaluations: 100
; Ratio (time for assembling + measure)/(total runtime for 100 evals): 0.05745164960182025
; number reverted permutation/ tried permutation: 15 / 51 =29.412%
; number reverted decision/ tried decision: 15 / 48 =31.250%

Equivalence checking error:
Unable to unify:
In environment:
(*symbolic_state*) {|
  dag_state :=
(*dag*)[
(*0*) (old 64 0, []);
(*1*) (old 64 1, []);
(*2*) (old 64 2, []);
(*3*) (old 64 3, []);
(*4*) (old 64 4, []);
(*5*) (const 19, []);
(*6*) (const 0, []);
(*7*) (mulZ, [0, 5]);
(*8*) (mul 64, [0, 5]);
(*9*) (const 2, []);
(*10*) (mulZ, [8, 9]);
(*11*) (const 38, []);
(*12*) (mul 64, [0, 11]);
(*13*) (mulZ, [0, 9]);
(*14*) (mul 64, [0, 9]);
(*15*) (mulZ, [1, 5]);
(*16*) (mul 64, [1, 5]);
(*17*) (mulZ, [9, 16]);
(*18*) (mul 64, [1, 11]);
(*19*) (mulZ, [1, 9]);
(*20*) (mul 64, [1, 9]);
(*21*) (mulZ, [2, 9]);
(*22*) (mul 64, [2, 9]);
(*23*) (mulZ, [3, 9]);
(*24*) (mul 64, [3, 9]);
(*25*) (const 18446744073709551616, []);
(*26*) (const 64, []);
(*27*) (mulZ, [0, 8]);
(*28*) (mul 64, [0, 0, 5]);
(*29*) (shrZ, [27, 26]);
(*30*) (shr 64, [27, 26]);
(*31*) (mulZ, [1, 12]);
(*32*) (mul 64, [0, 1, 11]);
(*33*) (shrZ, [31, 26]);
(*34*) (shr 64, [31, 26]);
(*35*) (mulZ, [1, 16]);
(*36*) (mul 64, [1, 1, 5]);
(*37*) (shrZ, [35, 26]);
(*38*) (shr 64, [35, 26]);
(*39*) (mulZ, [2, 12]);
(*40*) (mul 64, [0, 2, 11]);
(*41*) (shrZ, [39, 26]);
(*42*) (shr 64, [39, 26]);
(*43*) (mulZ, [2, 18]);
(*44*) (mul 64, [1, 2, 11]);
(*45*) (shrZ, [43, 26]);
(*46*) (shr 64, [43, 26]);
(*47*) (mulZ, [2, 2]);
(*48*) (mul 64, [2, 2]);
(*49*) (shrZ, [47, 26]);
(*50*) (shr 64, [47, 26]);
(*51*) (mulZ, [3, 12]);
(*52*) (mul 64, [0, 3, 11]);
(*53*) (shrZ, [51, 26]);
(*54*) (shr 64, [51, 26]);
(*55*) (mulZ, [3, 20]);
(*56*) (mul 64, [1, 3, 9]);
(*57*) (shrZ, [55, 26]);
(*58*) (shr 64, [55, 26]);
(*59*) (mulZ, [3, 22]);
(*60*) (mul 64, [2, 3, 9]);
(*61*) (shrZ, [59, 26]);
(*62*) (shr 64, [59, 26]);
(*63*) (mulZ, [3, 3]);
(*64*) (mul 64, [3, 3]);
(*65*) (shrZ, [63, 26]);
(*66*) (shr 64, [63, 26]);
(*67*) (mulZ, [4, 14]);
(*68*) (mul 64, [0, 4, 9]);
(*69*) (shrZ, [67, 26]);
(*70*) (shr 64, [67, 26]);
(*71*) (mulZ, [4, 20]);
(*72*) (mul 64, [1, 4, 9]);
(*73*) (shrZ, [71, 26]);
(*74*) (shr 64, [71, 26]);
(*75*) (mulZ, [4, 22]);
(*76*) (mul 64, [2, 4, 9]);
(*77*) (shrZ, [75, 26]);
(*78*) (shr 64, [75, 26]);
(*79*) (mulZ, [4, 24]);
(*80*) (mul 64, [3, 4, 9]);
(*81*) (shrZ, [79, 26]);
(*82*) (shr 64, [79, 26]);
(*83*) (mulZ, [4, 4]);
(*84*) (mul 64, [4, 4]);
(*85*) (shrZ, [83, 26]);
(*86*) (shr 64, [83, 26]);
(*87*) (add 64, [44, 52]);
(*88*) (addcarryZ 64, [52, 44]);
(*89*) (addcarry 64, [44, 52]);
(*90*) (add 64, [46, 54, 89]);
(*91*) (addcarryZ 64, [89, 54, 46]);
(*92*) (addcarry 64, [46, 54, 89]);
(*93*) (add 64, [44, 52, 84]);
(*94*) (addcarryZ 64, [84, 87]);
(*95*) (addcarry 64, [84, 87]);
(*96*) (add 64, [46, 54, 86, 89, 95]);
(*97*) (addcarryZ 64, [95, 86, 90]);
(*98*) (addcarry 64, [86, 90, 95]);
(*99*) (const 13, []);
(*100*) (const 8192, []);
(*101*) (mul 64, [96, 100]);
(*102*) (const 51, []);
(*103*) (shrZ, [93, 102]);
(*104*) (shr 64, [93, 102]);
(*105*) (orZ, [101, 104]);
(*106*) (or 64, [101, 104]);
(*107*) (const 2251799813685247, []);
(*108*) (slice 0 51, [93]);
(*109*) (add 64, [48, 56]);
(*110*) (addcarryZ 64, [56, 48]);
(*111*) (addcarry 64, [48, 56]);
(*112*) (add 64, [50, 58, 111]);
(*113*) (addcarryZ 64, [111, 58, 50]);
(*114*) (addcarry 64, [50, 58, 111]);
(*115*) (add 64, [48, 56, 68]);
(*116*) (addcarryZ 64, [68, 109]);
(*117*) (addcarry 64, [68, 109]);
(*118*) (add 64, [50, 58, 70, 111, 117]);
(*119*) (addcarryZ 64, [117, 70, 112]);
(*120*) (addcarry 64, [70, 112, 117]);
(*121*) (add 64, [28, 60]);
(*122*) (addcarryZ 64, [60, 28]);
(*123*) (addcarry 64, [28, 60]);
(*124*) (add 64, [30, 62, 123]);
(*125*) (addcarryZ 64, [123, 62, 30]);
(*126*) (addcarry 64, [30, 62, 123]);
(*127*) (add 64, [28, 60, 72]);
(*128*) (addcarryZ 64, [72, 121]);
(*129*) (addcarry 64, [72, 121]);
(*130*) (add 64, [30, 62, 74, 123, 129]);
(*131*) (addcarryZ 64, [129, 74, 124]);
(*132*) (addcarry 64, [74, 124, 129]);
(*133*) (add 64, [32, 64]);
(*134*) (addcarryZ 64, [64, 32]);
(*135*) (addcarry 64, [32, 64]);
(*136*) (add 64, [34, 66, 135]);
(*137*) (addcarryZ 64, [135, 66, 34]);
(*138*) (addcarry 64, [34, 66, 135]);
(*139*) (add 64, [32, 64, 76]);
(*140*) (addcarryZ 64, [76, 133]);
(*141*) (addcarry 64, [76, 133]);
(*142*) (add 64, [34, 66, 78, 135, 141]);
(*143*) (addcarryZ 64, [141, 78, 136]);
(*144*) (addcarry 64, [78, 136, 141]);
(*145*) (add 64, [36, 40]);
(*146*) (addcarryZ 64, [40, 36]);
(*147*) (addcarry 64, [36, 40]);
(*148*) (add 64, [38, 42, 147]);
(*149*) (addcarryZ 64, [147, 42, 38]);
(*150*) (addcarry 64, [38, 42, 147]);
(*151*) (add 64, [36, 40, 80]);
(*152*) (addcarryZ 64, [80, 145]);
(*153*) (addcarry 64, [80, 145]);
(*154*) (add 64, [38, 42, 82, 147, 153]);
(*155*) (addcarryZ 64, [153, 82, 148]);
(*156*) (addcarry 64, [82, 148, 153]);
(*157*) (add 64, [36, 40, 80, 106]);
(*158*) (addcarryZ 64, [106, 151]);
(*159*) (addcarry 64, [106, 151]);
(*160*) (addZ, [159, 154]);
(*161*) (add 64, [38, 42, 82, 147, 153, 159]);
(*162*) (mul 64, [100, 161]);
(*163*) (shrZ, [157, 102]);
(*164*) (shr 64, [157, 102]);
(*165*) (orZ, [162, 164]);
(*166*) (or 64, [162, 164]);
(*167*) (slice 0 51, [157]);
(*168*) (add 64, [32, 64, 76, 166]);
(*169*) (addcarryZ 64, [166, 139]);
(*170*) (addcarry 64, [139, 166]);
(*171*) (addZ, [170, 142]);
(*172*) (add 64, [34, 66, 78, 135, 141, 170]);
(*173*) (mul 64, [100, 172]);
(*174*) (shrZ, [168, 102]);
(*175*) (shr 64, [168, 102]);
(*176*) (orZ, [173, 175]);
(*177*) (or 64, [173, 175]);
(*178*) (slice 0 51, [168]);
(*179*) (add 64, [28, 60, 72, 177]);
(*180*) (addcarryZ 64, [177, 127]);
(*181*) (addcarry 64, [127, 177]);
(*182*) (addZ, [181, 130]);
(*183*) (add 64, [30, 62, 74, 123, 129, 181]);
(*184*) (mul 64, [100, 183]);
(*185*) (shrZ, [179, 102]);
(*186*) (shr 64, [179, 102]);
(*187*) (orZ, [184, 186]);
(*188*) (or 64, [184, 186]);
(*189*) (slice 0 51, [179]);
(*190*) (add 64, [48, 56, 68, 188]);
(*191*) (addcarryZ 64, [188, 115]);
(*192*) (addcarry 64, [115, 188]);
(*193*) (addZ, [192, 118]);
(*194*) (add 64, [50, 58, 70, 111, 117, 192]);
(*195*) (mul 64, [100, 194]);
(*196*) (shrZ, [190, 102]);
(*197*) (shr 64, [190, 102]);
(*198*) (orZ, [195, 197]);
(*199*) (or 64, [195, 197]);
(*200*) (slice 0 51, [190]);
(*201*) (mulZ, [5, 199]);
(*202*) (mul 64, [5, 199]);
(*203*) (addZ, [108, 202]);
(*204*) (add 64, [108, 202]);
(*205*) (shrZ, [204, 102]);
(*206*) (shr 64, [204, 102]);
(*207*) (slice 0 51, [204]);
(*208*) (addZ, [206, 167]);
(*209*) (add 64, [167, 206]);
(*210*) (shrZ, [209, 102]);
(*211*) (shr 64, [209, 102]);
(*212*) (slice 0 51, [209]);
(*213*) (addZ, [211, 178]);
(*214*) (add 64, [178, 211]);
(*215*) (old 64 215, []);
(*216*) (old 64 216, []);
(*217*) (old 64 217, []);
(*218*) (old 64 218, []);
(*219*) (old 64 219, []);
(*220*) (old 64 220, []);
(*221*) (old 64 221, []);
(*222*) (old 64 222, []);
(*223*) (old 64 223, []);
(*224*) (old 64 224, []);
(*225*) (old 64 225, []);
(*226*) (old 64 226, []);
(*227*) (old 64 227, []);
(*228*) (old 64 228, []);
(*229*) (old 64 229, []);
(*230*) (old 64 230, []);
(*231*) (old 64 231, []);
(*232*) (old 64 232, []);
(*233*) (old 64 233, []);
(*234*) (old 64 234, []);
(*235*) (old 64 235, []);
(*236*) (old 64 236, []);
(*237*) (const 8, []);
(*238*) (add 64, [236, 237]);
(*239*) (const 16, []);
(*240*) (add 64, [236, 239]);
(*241*) (const 24, []);
(*242*) (add 64, [236, 241]);
(*243*) (const 32, []);
(*244*) (add 64, [236, 243]);
(*245*) (old 64 245, []);
(*246*) (add 64, [237, 245]);
(*247*) (add 64, [239, 245]);
(*248*) (add 64, [241, 245]);
(*249*) (add 64, [243, 245]);
(*250*) (old 64 250, []);
(*251*) (old 64 251, []);
(*252*) (old 64 252, []);
(*253*) (old 64 253, []);
(*254*) (old 64 254, []);
(*255*) (old 64 255, []);
(*256*) (old 64 256, []);
(*257*) (old 64 257, []);
(*258*) (old 64 258, []);
(*259*) (old 64 259, []);
(*260*) (old 64 260, []);
(*261*) (old 64 261, []);
(*262*) (old 64 262, []);
(*263*) (old 64 263, []);
(*264*) (old 64 264, []);
(*265*) (old 64 265, []);
(*266*) (old 64 266, []);
(*267*) (old 64 267, []);
(*268*) (old 64 268, []);
(*269*) (old 64 269, []);
(*270*) (old 64 270, []);
(*271*) (old 64 271, []);
(*272*) (old 64 272, []);
(*273*) (old 64 273, []);
(*274*) (old 64 274, []);
(*275*) (old 64 275, []);
(*276*) (old 64 276, []);
(*277*) (old 64 277, []);
(*278*) (old 64 278, []);
(*279*) (old 64 279, []);
(*280*) (old 64 280, []);
(*281*) (old 64 281, []);
(*282*) (old 64 282, []);
(*283*) (old 64 283, []);
(*284*) (old 64 284, []);
(*285*) (old 64 285, []);
(*286*) (old 64 286, []);
(*287*) (old 64 287, []);
(*288*) (old 64 288, []);
(*289*) (old 64 289, []);
(*290*) (old 64 290, []);
(*291*) (old 64 291, []);
(*292*) (old 64 292, []);
(*293*) (old 64 293, []);
(*294*) (old 64 294, []);
(*295*) (old 64 295, []);
(*296*) (old 64 296, []);
(*297*) (old 64 297, []);
(*298*) (old 64 298, []);
(*299*) (old 64 299, []);
(*300*) (old 64 300, []);
(*301*) (old 64 301, []);
(*302*) (old 64 302, []);
(*303*) (old 64 303, []);
(*304*) (old 64 304, []);
(*305*) (old 64 305, []);
(*306*) (old 64 306, []);
(*307*) (old 64 307, []);
(*308*) (old 64 308, []);
(*309*) (old 64 309, []);
(*310*) (old 64 310, []);
(*311*) (old 64 311, []);
(*312*) (old 64 312, []);
(*313*) (old 64 313, []);
(*314*) (old 64 314, []);
(*315*) (old 64 315, []);
(*316*) (old 64 316, []);
(*317*) (old 64 317, []);
(*318*) (old 64 318, []);
(*319*) (old 64 319, []);
(*320*) (old 64 320, []);
(*321*) (old 64 321, []);
(*322*) (old 64 322, []);
(*323*) (old 64 323, []);
(*324*) (old 64 324, []);
(*325*) (old 64 325, []);
(*326*) (old 64 326, []);
(*327*) (old 64 327, []);
(*328*) (old 64 328, []);
(*329*) (old 64 329, []);
(*330*) (old 64 330, []);
(*331*) (old 64 331, []);
(*332*) (old 64 332, []);
(*333*) (old 64 333, []);
(*334*) (old 64 334, []);
(*335*) (old 64 335, []);
(*336*) (old 64 336, []);
(*337*) (old 64 337, []);
(*338*) (old 64 338, []);
(*339*) (old 64 339, []);
(*340*) (old 64 340, []);
(*341*) (old 64 341, []);
(*342*) (old 64 342, []);
(*343*) (old 64 343, []);
(*344*) (old 64 344, []);
(*345*) (old 64 345, []);
(*346*) (old 64 346, []);
(*347*) (old 64 347, []);
(*348*) (old 64 348, []);
(*349*) (old 64 349, []);
(*350*) (old 64 350, []);
(*351*) (old 64 351, []);
(*352*) (old 64 352, []);
(*353*) (old 64 353, []);
(*354*) (old 64 354, []);
(*355*) (old 64 355, []);
(*356*) (old 64 356, []);
(*357*) (old 64 357, []);
(*358*) (old 64 358, []);
(*359*) (old 64 359, []);
(*360*) (old 64 360, []);
(*361*) (old 64 361, []);
(*362*) (old 64 362, []);
(*363*) (old 64 363, []);
(*364*) (old 64 364, []);
(*365*) (old 64 365, []);
(*366*) (old 64 366, []);
(*367*) (old 64 367, []);
(*368*) (old 64 368, []);
(*369*) (old 64 369, []);
(*370*) (old 64 370, []);
(*371*) (old 64 371, []);
(*372*) (old 64 372, []);
(*373*) (old 64 373, []);
(*374*) (old 64 374, []);
(*375*) (old 64 375, []);
(*376*) (old 64 376, []);
(*377*) (old 64 377, []);
(*378*) (old 64 378, []);
(*379*) (old 64 379, []);
(*380*) (old 64 380, []);
(*381*) (old 64 381, []);
(*382*) (old 64 382, []);
(*383*) (old 64 383, []);
(*384*) (old 64 384, []);
(*385*) (old 64 385, []);
(*386*) (old 64 386, []);
(*387*) (old 64 387, []);
(*388*) (old 64 388, []);
(*389*) (old 64 389, []);
(*390*) (old 64 390, []);
(*391*) (old 64 391, []);
(*392*) (old 64 392, []);
(*393*) (old 64 393, []);
(*394*) (old 64 394, []);
(*395*) (old 64 395, []);
(*396*) (old 64 396, []);
(*397*) (old 64 397, []);
(*398*) (old 64 398, []);
(*399*) (old 64 399, []);
(*400*) (old 64 400, []);
(*401*) (old 64 401, []);
(*402*) (old 64 402, []);
(*403*) (const 18446744073709550400, []);
(*404*) (add 64, [402, 403]);
(*405*) (const 18446744073709550408, []);
(*406*) (add 64, [402, 405]);
(*407*) (const 18446744073709550416, []);
(*408*) (add 64, [402, 407]);
(*409*) (const 18446744073709550424, []);
(*410*) (add 64, [402, 409]);
(*411*) (const 18446744073709550432, []);
(*412*) (add 64, [402, 411]);
(*413*) (const 40, []);
(*414*) (const 18446744073709550440, []);
(*415*) (add 64, [402, 414]);
(*416*) (const 48, []);
(*417*) (const 18446744073709550448, []);
(*418*) (add 64, [402, 417]);
(*419*) (const 56, []);
(*420*) (const 18446744073709550456, []);
(*421*) (add 64, [402, 420]);
(*422*) (const 18446744073709550464, []);
(*423*) (add 64, [402, 422]);
(*424*) (const 72, []);
(*425*) (const 18446744073709550472, []);
(*426*) (add 64, [402, 425]);
(*427*) (const 80, []);
(*428*) (const 18446744073709550480, []);
(*429*) (add 64, [402, 428]);
(*430*) (const 88, []);
(*431*) (const 18446744073709550488, []);
(*432*) (add 64, [402, 431]);
(*433*) (const 96, []);
(*434*) (const 18446744073709550496, []);
(*435*) (add 64, [402, 434]);
(*436*) (const 104, []);
(*437*) (const 18446744073709550504, []);
(*438*) (add 64, [402, 437]);
(*439*) (const 112, []);
(*440*) (const 18446744073709550512, []);
(*441*) (add 64, [402, 440]);
(*442*) (const 120, []);
(*443*) (const 18446744073709550520, []);
(*444*) (add 64, [402, 443]);
(*445*) (const 128, []);
(*446*) (const 18446744073709550528, []);
(*447*) (add 64, [402, 446]);
(*448*) (const 136, []);
(*449*) (const 18446744073709550536, []);
(*450*) (add 64, [402, 449]);
(*451*) (const 144, []);
(*452*) (const 18446744073709550544, []);
(*453*) (add 64, [402, 452]);
(*454*) (const 152, []);
(*455*) (const 18446744073709550552, []);
(*456*) (add 64, [402, 455]);
(*457*) (const 160, []);
(*458*) (const 18446744073709550560, []);
(*459*) (add 64, [402, 458]);
(*460*) (const 168, []);
(*461*) (const 18446744073709550568, []);
(*462*) (add 64, [402, 461]);
(*463*) (const 176, []);
(*464*) (const 18446744073709550576, []);
(*465*) (add 64, [402, 464]);
(*466*) (const 184, []);
(*467*) (const 18446744073709550584, []);
(*468*) (add 64, [402, 467]);
(*469*) (const 192, []);
(*470*) (const 18446744073709550592, []);
(*471*) (add 64, [402, 470]);
(*472*) (const 200, []);
(*473*) (const 18446744073709550600, []);
(*474*) (add 64, [402, 473]);
(*475*) (const 208, []);
(*476*) (const 18446744073709550608, []);
(*477*) (add 64, [402, 476]);
(*478*) (const 216, []);
(*479*) (const 18446744073709550616, []);
(*480*) (add 64, [402, 479]);
(*481*) (const 224, []);
(*482*) (const 18446744073709550624, []);
(*483*) (add 64, [402, 482]);
(*484*) (const 232, []);
(*485*) (const 18446744073709550632, []);
(*486*) (add 64, [402, 485]);
(*487*) (const 240, []);
(*488*) (const 18446744073709550640, []);
(*489*) (add 64, [402, 488]);
(*490*) (const 248, []);
(*491*) (const 18446744073709550648, []);
(*492*) (add 64, [402, 491]);
(*493*) (const 256, []);
(*494*) (const 18446744073709550656, []);
(*495*) (add 64, [402, 494]);
(*496*) (const 264, []);
(*497*) (const 18446744073709550664, []);
(*498*) (add 64, [402, 497]);
(*499*) (const 272, []);
(*500*) (const 18446744073709550672, []);
(*501*) (add 64, [402, 500]);
(*502*) (const 280, []);
(*503*) (const 18446744073709550680, []);
(*504*) (add 64, [402, 503]);
(*505*) (const 288, []);
(*506*) (const 18446744073709550688, []);
(*507*) (add 64, [402, 506]);
(*508*) (const 296, []);
(*509*) (const 18446744073709550696, []);
(*510*) (add 64, [402, 509]);
(*511*) (const 304, []);
(*512*) (const 18446744073709550704, []);
(*513*) (add 64, [402, 512]);
(*514*) (const 312, []);
(*515*) (const 18446744073709550712, []);
(*516*) (add 64, [402, 515]);
(*517*) (const 320, []);
(*518*) (const 18446744073709550720, []);
(*519*) (add 64, [402, 518]);
(*520*) (const 328, []);
(*521*) (const 18446744073709550728, []);
(*522*) (add 64, [402, 521]);
(*523*) (const 336, []);
(*524*) (const 18446744073709550736, []);
(*525*) (add 64, [402, 524]);
(*526*) (const 344, []);
(*527*) (const 18446744073709550744, []);
(*528*) (add 64, [402, 527]);
(*529*) (const 352, []);
(*530*) (const 18446744073709550752, []);
(*531*) (add 64, [402, 530]);
(*532*) (const 360, []);
(*533*) (const 18446744073709550760, []);
(*534*) (add 64, [402, 533]);
(*535*) (const 368, []);
(*536*) (const 18446744073709550768, []);
(*537*) (add 64, [402, 536]);
(*538*) (const 376, []);
(*539*) (const 18446744073709550776, []);
(*540*) (add 64, [402, 539]);
(*541*) (const 384, []);
(*542*) (const 18446744073709550784, []);
(*543*) (add 64, [402, 542]);
(*544*) (const 392, []);
(*545*) (const 18446744073709550792, []);
(*546*) (add 64, [402, 545]);
(*547*) (const 400, []);
(*548*) (const 18446744073709550800, []);
(*549*) (add 64, [402, 548]);
(*550*) (const 408, []);
(*551*) (const 18446744073709550808, []);
(*552*) (add 64, [402, 551]);
(*553*) (const 416, []);
(*554*) (const 18446744073709550816, []);
(*555*) (add 64, [402, 554]);
(*556*) (const 424, []);
(*557*) (const 18446744073709550824, []);
(*558*) (add 64, [402, 557]);
(*559*) (const 432, []);
(*560*) (const 18446744073709550832, []);
(*561*) (add 64, [402, 560]);
(*562*) (const 440, []);
(*563*) (const 18446744073709550840, []);
(*564*) (add 64, [402, 563]);
(*565*) (const 448, []);
(*566*) (const 18446744073709550848, []);
(*567*) (add 64, [402, 566]);
(*568*) (const 456, []);
(*569*) (const 18446744073709550856, []);
(*570*) (add 64, [402, 569]);
(*571*) (const 464, []);
(*572*) (const 18446744073709550864, []);
(*573*) (add 64, [402, 572]);
(*574*) (const 472, []);
(*575*) (const 18446744073709550872, []);
(*576*) (add 64, [402, 575]);
(*577*) (const 480, []);
(*578*) (const 18446744073709550880, []);
(*579*) (add 64, [402, 578]);
(*580*) (const 488, []);
(*581*) (const 18446744073709550888, []);
(*582*) (add 64, [402, 581]);
(*583*) (const 496, []);
(*584*) (const 18446744073709550896, []);
(*585*) (add 64, [402, 584]);
(*586*) (const 504, []);
(*587*) (const 18446744073709550904, []);
(*588*) (add 64, [402, 587]);
(*589*) (const 512, []);
(*590*) (const 18446744073709550912, []);
(*591*) (add 64, [402, 590]);
(*592*) (const 520, []);
(*593*) (const 18446744073709550920, []);
(*594*) (add 64, [402, 593]);
(*595*) (const 528, []);
(*596*) (const 18446744073709550928, []);
(*597*) (add 64, [402, 596]);
(*598*) (const 536, []);
(*599*) (const 18446744073709550936, []);
(*600*) (add 64, [402, 599]);
(*601*) (const 544, []);
(*602*) (const 18446744073709550944, []);
(*603*) (add 64, [402, 602]);
(*604*) (const 552, []);
(*605*) (const 18446744073709550952, []);
(*606*) (add 64, [402, 605]);
(*607*) (const 560, []);
(*608*) (const 18446744073709550960, []);
(*609*) (add 64, [402, 608]);
(*610*) (const 568, []);
(*611*) (const 18446744073709550968, []);
(*612*) (add 64, [402, 611]);
(*613*) (const 576, []);
(*614*) (const 18446744073709550976, []);
(*615*) (add 64, [402, 614]);
(*616*) (const 584, []);
(*617*) (const 18446744073709550984, []);
(*618*) (add 64, [402, 617]);
(*619*) (const 592, []);
(*620*) (const 18446744073709550992, []);
(*621*) (add 64, [402, 620]);
(*622*) (const 600, []);
(*623*) (const 18446744073709551000, []);
(*624*) (add 64, [402, 623]);
(*625*) (const 608, []);
(*626*) (const 18446744073709551008, []);
(*627*) (add 64, [402, 626]);
(*628*) (const 616, []);
(*629*) (const 18446744073709551016, []);
(*630*) (add 64, [402, 629]);
(*631*) (const 624, []);
(*632*) (const 18446744073709551024, []);
(*633*) (add 64, [402, 632]);
(*634*) (const 632, []);
(*635*) (const 18446744073709551032, []);
(*636*) (add 64, [402, 635]);
(*637*) (const 640, []);
(*638*) (const 18446744073709551040, []);
(*639*) (add 64, [402, 638]);
(*640*) (const 648, []);
(*641*) (const 18446744073709551048, []);
(*642*) (add 64, [402, 641]);
(*643*) (const 656, []);
(*644*) (const 18446744073709551056, []);
(*645*) (add 64, [402, 644]);
(*646*) (const 664, []);
(*647*) (const 18446744073709551064, []);
(*648*) (add 64, [402, 647]);
(*649*) (const 672, []);
(*650*) (const 18446744073709551072, []);
(*651*) (add 64, [402, 650]);
(*652*) (const 680, []);
(*653*) (const 18446744073709551080, []);
(*654*) (add 64, [402, 653]);
(*655*) (const 688, []);
(*656*) (const 18446744073709551088, []);
(*657*) (add 64, [402, 656]);
(*658*) (const 696, []);
(*659*) (const 18446744073709551096, []);
(*660*) (add 64, [402, 659]);
(*661*) (const 704, []);
(*662*) (const 18446744073709551104, []);
(*663*) (add 64, [402, 662]);
(*664*) (const 712, []);
(*665*) (const 18446744073709551112, []);
(*666*) (add 64, [402, 665]);
(*667*) (const 720, []);
(*668*) (const 18446744073709551120, []);
(*669*) (add 64, [402, 668]);
(*670*) (const 728, []);
(*671*) (const 18446744073709551128, []);
(*672*) (add 64, [402, 671]);
(*673*) (const 736, []);
(*674*) (const 18446744073709551136, []);
(*675*) (add 64, [402, 674]);
(*676*) (const 744, []);
(*677*) (const 18446744073709551144, []);
(*678*) (add 64, [402, 677]);
(*679*) (const 752, []);
(*680*) (const 18446744073709551152, []);
(*681*) (add 64, [402, 680]);
(*682*) (const 760, []);
(*683*) (const 18446744073709551160, []);
(*684*) (add 64, [402, 683]);
(*685*) (const 768, []);
(*686*) (const 18446744073709551168, []);
(*687*) (add 64, [402, 686]);
(*688*) (const 776, []);
(*689*) (const 18446744073709551176, []);
(*690*) (add 64, [402, 689]);
(*691*) (const 784, []);
(*692*) (const 18446744073709551184, []);
(*693*) (add 64, [402, 692]);
(*694*) (const 792, []);
(*695*) (const 18446744073709551192, []);
(*696*) (add 64, [402, 695]);
(*697*) (const 800, []);
(*698*) (const 18446744073709551200, []);
(*699*) (add 64, [402, 698]);
(*700*) (const 808, []);
(*701*) (const 18446744073709551208, []);
(*702*) (add 64, [402, 701]);
(*703*) (const 816, []);
(*704*) (const 18446744073709551216, []);
(*705*) (add 64, [402, 704]);
(*706*) (const 824, []);
(*707*) (const 18446744073709551224, []);
(*708*) (add 64, [402, 707]);
(*709*) (const 832, []);
(*710*) (const 18446744073709551232, []);
(*711*) (add 64, [402, 710]);
(*712*) (const 840, []);
(*713*) (const 18446744073709551240, []);
(*714*) (add 64, [402, 713]);
(*715*) (const 848, []);
(*716*) (const 18446744073709551248, []);
(*717*) (add 64, [402, 716]);
(*718*) (const 856, []);
(*719*) (const 18446744073709551256, []);
(*720*) (add 64, [402, 719]);
(*721*) (const 864, []);
(*722*) (const 18446744073709551264, []);
(*723*) (add 64, [402, 722]);
(*724*) (const 872, []);
(*725*) (const 18446744073709551272, []);
(*726*) (add 64, [402, 725]);
(*727*) (const 880, []);
(*728*) (const 18446744073709551280, []);
(*729*) (add 64, [402, 728]);
(*730*) (const 888, []);
(*731*) (const 18446744073709551288, []);
(*732*) (add 64, [402, 731]);
(*733*) (const 896, []);
(*734*) (const 18446744073709551296, []);
(*735*) (add 64, [402, 734]);
(*736*) (const 904, []);
(*737*) (const 18446744073709551304, []);
(*738*) (add 64, [402, 737]);
(*739*) (const 912, []);
(*740*) (const 18446744073709551312, []);
(*741*) (add 64, [402, 740]);
(*742*) (const 920, []);
(*743*) (const 18446744073709551320, []);
(*744*) (add 64, [402, 743]);
(*745*) (const 928, []);
(*746*) (const 18446744073709551328, []);
(*747*) (add 64, [402, 746]);
(*748*) (const 936, []);
(*749*) (const 18446744073709551336, []);
(*750*) (add 64, [402, 749]);
(*751*) (const 944, []);
(*752*) (const 18446744073709551344, []);
(*753*) (add 64, [402, 752]);
(*754*) (const 952, []);
(*755*) (const 18446744073709551352, []);
(*756*) (add 64, [402, 755]);
(*757*) (const 960, []);
(*758*) (const 18446744073709551360, []);
(*759*) (add 64, [402, 758]);
(*760*) (const 968, []);
(*761*) (const 18446744073709551368, []);
(*762*) (add 64, [402, 761]);
(*763*) (const 976, []);
(*764*) (const 18446744073709551376, []);
(*765*) (add 64, [402, 764]);
(*766*) (const 984, []);
(*767*) (const 18446744073709551384, []);
(*768*) (add 64, [402, 767]);
(*769*) (const 992, []);
(*770*) (const 18446744073709551392, []);
(*771*) (add 64, [402, 770]);
(*772*) (const 1000, []);
(*773*) (const 18446744073709551400, []);
(*774*) (add 64, [402, 773]);
(*775*) (const 1008, []);
(*776*) (const 18446744073709551408, []);
(*777*) (add 64, [402, 776]);
(*778*) (const 1016, []);
(*779*) (const 18446744073709551416, []);
(*780*) (add 64, [402, 779]);
(*781*) (const 1024, []);
(*782*) (const 18446744073709551424, []);
(*783*) (add 64, [402, 782]);
(*784*) (const 1032, []);
(*785*) (const 18446744073709551432, []);
(*786*) (add 64, [402, 785]);
(*787*) (const 1040, []);
(*788*) (const 18446744073709551440, []);
(*789*) (add 64, [402, 788]);
(*790*) (const 1048, []);
(*791*) (const 18446744073709551448, []);
(*792*) (add 64, [402, 791]);
(*793*) (const 1056, []);
(*794*) (const 18446744073709551456, []);
(*795*) (add 64, [402, 794]);
(*796*) (const 1064, []);
(*797*) (const 18446744073709551464, []);
(*798*) (add 64, [402, 797]);
(*799*) (const 1072, []);
(*800*) (const 18446744073709551472, []);
(*801*) (add 64, [402, 800]);
(*802*) (const 1080, []);
(*803*) (const 18446744073709551480, []);
(*804*) (add 64, [402, 803]);
(*805*) (const 1088, []);
(*806*) (const 18446744073709551488, []);
(*807*) (add 64, [402, 806]);
(*808*) (const 1096, []);
(*809*) (const 18446744073709551496, []);
(*810*) (add 64, [402, 809]);
(*811*) (const 1104, []);
(*812*) (const 18446744073709551504, []);
(*813*) (add 64, [402, 812]);
(*814*) (const 1112, []);
(*815*) (const 18446744073709551512, []);
(*816*) (add 64, [402, 815]);
(*817*) (const 1120, []);
(*818*) (const 18446744073709551520, []);
(*819*) (add 64, [402, 818]);
(*820*) (const 1128, []);
(*821*) (const 18446744073709551528, []);
(*822*) (add 64, [402, 821]);
(*823*) (const 1136, []);
(*824*) (const 18446744073709551536, []);
(*825*) (add 64, [402, 824]);
(*826*) (const 1144, []);
(*827*) (const 18446744073709551544, []);
(*828*) (add 64, [402, 827]);
(*829*) (const 1152, []);
(*830*) (const 18446744073709551552, []);
(*831*) (add 64, [402, 830]);
(*832*) (const 1160, []);
(*833*) (const 18446744073709551560, []);
(*834*) (add 64, [402, 833]);
(*835*) (const 1168, []);
(*836*) (const 18446744073709551568, []);
(*837*) (add 64, [402, 836]);
(*838*) (const 1176, []);
(*839*) (const 18446744073709551576, []);
(*840*) (add 64, [402, 839]);
(*841*) (const 1184, []);
(*842*) (const 18446744073709551584, []);
(*843*) (add 64, [402, 842]);
(*844*) (const 1192, []);
(*845*) (const 18446744073709551592, []);
(*846*) (add 64, [402, 845]);
(*847*) (const 1200, []);
(*848*) (const 18446744073709551600, []);
(*849*) (add 64, [402, 848]);
(*850*) (const 1208, []);
(*851*) (const 18446744073709551608, []);
(*852*) (add 64, [402, 851]);
(*853*) (subborrow 64, [402, 454]);
(*854*) (const 1, []);
(*855*) (const 63, []);
(*856*) (mulZ, [1, 11]);
(*857*) (add 64, [22]);
(*858*) (mul 64, [0, 237]);
(*859*) (const 9, []);
(*860*) (mul 64, [0, 859]);
(*861*) (add 64, [860]);
(*862*) (const 18, []);
(*863*) (mul 64, [0, 862]);
(*864*) (add 64, [8]);
(*865*) (add 64, [14]);
(*866*) (xorZ, [24, 24]);
(*867*) (mulZ, [0, 11]);
(*868*) (slice 0 8, [18]);
(*869*) (iszero, [868]);
(*870*) (slice 0 8, [44]);
(*871*) (iszero, [870]);
(*872*) (xorZ, [20, 20]);
(*873*) (const -51, []);
(*874*) (addoverflow 64, [36, 40]);
(*875*) (xorZ, [40, 40]);
(*876*) (addcarry 64, [154, 159]);
(*877*) (addoverflow 64, [154, 159]);
(*878*) (slice 0 8, [93]);
(*879*) (iszero, [878]);
(*880*) (addcarry 64, [142, 170]);
(*881*) (xorZ, [96, 96]);
(*882*) (addcarry 64, [130, 181]);
(*883*) (xorZ, [106, 106]);
(*884*) (addcarry 64, [118, 192]);
(*885*) (mul 64, [199, 237]);
(*886*) (add 64, [199, 885]);
(*887*) (mul 64, [9, 886]);
(*888*) (add 64, [199, 887]);
(*889*) (add 64, [108, 199, 887]);
(*890*) (slice 0 51, [889]);
(*891*) (shr 64, [889, 102]);
(*892*) (add 64, [167, 891]);
(*893*) (shr 64, [892, 102]);
(*894*) (add 64, [178, 893]);
(*895*) (slice 0 51, [892]);
(*896*) (addcarry 64, [454, 798]);
(*897*) (addoverflow 64, [454, 798]);
]
;
  symbolic_reg_state := [(rax, 236), (rcx, 894), (rdx, 199), (rbx, 218), (rsp, 402), (rbp, 220), (rsi, 245), (rdi, 189), (r8, 888), (r9, 6), (r10, 167), (r11, 890), (r12, 227), (r13, 228), (r14, 229), (r15, 230)];
  symbolic_flag_state := (*flag_state*)(CF=Some 896 PF=None AF=None ZF=None SF=None ZF=None OF=Some 897);
  symbolic_mem_state :=
[(852, 42), (849, 54), (846, 84), (843, 80), (840, 82), (837, 72), (834, 74), (831, 121), (828, 124), (825, 86), (822, 36), (819, 38), (816, 236), (813, 230), (810, 229), (807, 228), (804, 227), (801, 220), (798, 218), (795, 269), (792, 270), (789, 271), (786, 272), (783, 273), (780, 274), (777, 275), (774, 276), (771, 277), (768, 278), (765, 279), (762, 280), (759, 281), (756, 282), (753, 283), (750, 284), (747, 285), (744, 286), (741, 287), (738, 288), (735, 289), (732, 290), (729, 291), (726, 292), (723, 293), (720, 294), (717, 295), (714, 296), (711, 297), (708, 298), (705, 299), (702, 300), (699, 301), (696, 302), (693, 303), (690, 304), (687, 305), (684, 306), (681, 307), (678, 308), (675, 309), (672, 310), (669, 311), (666, 312), (663, 313), (660, 314), (657, 315), (654, 316), (651, 317), (648, 318), (645, 319), (642, 320), (639, 321), (636, 322), (633, 323), (630, 324), (627, 325), (624, 326), (621, 327), (618, 328), (615, 329), (612, 330), (609, 331), (606, 332), (603, 333), (600, 334), (597, 335), (594, 336), (591, 337), (588, 338), (585, 339), (582, 340), (579, 341), (576, 342), (573, 343), (570, 344), (567, 345), (564, 346), (561, 347), (558, 348), (555, 349), (552, 350), (549, 351), (546, 352), (543, 353), (540, 354), (537, 355), (534, 356), (531, 357), (528, 358), (525, 359), (522, 360), (519, 361), (516, 362), (513, 363), (510, 364), (507, 365), (504, 366), (501, 367), (498, 368), (495, 369), (492, 370), (489, 371), (486, 372), (483, 373), (480, 374), (477, 375), (474, 376), (471, 377), (468, 378), (465, 379), (462, 380), (459, 381), (456, 382), (453, 383), (450, 384), (447, 385), (444, 386), (441, 387), (438, 388), (435, 389), (432, 390), (429, 391), (426, 392), (423, 393), (421, 394), (418, 395), (415, 396), (412, 397), (410, 398), (408, 399), (406, 400), (404, 401), (249, 0), (248, 1), (247, 2), (246, 3), (245, 4), (244, 200), (242, 189), (240, 894), (238, 895), (236, 890)]
;
|}
Unable to unify: [inr [890, 895, 894, 189, 200]] == [inr [207, 212, 214, 189, 200]]
Could not unify the values at index 0: [#890, #895, #894, #189, #200] != [#207, #212, #214, #189, #200]
index 0: #890 != #207
(slice 0 51, [#889]) != (slice 0 51, [#204])
index 0: #889 != #204
(add 64, [#108, #199, #887]) != (add 64, [#108, #202])
(add 64, [#199, #887]) != (add 64, [#202])
(add 64, [#199, (mul 64, [#9, #886])]) != (add 64, [(mul 64, [#5, #199])])
(add 64, [#199, (mul 64, [#9, (add 64, [#199, #885])])]) != (add 64, [(mul 64, [#5, #199])])
(add 64, [#199, (mul 64, [#9, (add 64, [#199, (mul 64, [#199, #237])])])]) != (add 64, [(mul 64, [#5, #199])])
(add 64, [#199, (mul 64, [#9, (add 64, [#199, (mul 64, [#199, (const 8, [])])])])]) != (add 64, [(mul 64, [#5, #199])])
(add 64, [(or 64, [#195, #197]), (mul 64, [(const 2, []), (add 64, [(or 64, [#195, #197]), (mul 64, [(or 64, [#195, #197]), (const 8, [])])])])]) != (add 64, [(mul 64, [(const 19, []), (or 64, [#195, #197])])])