sarx eax, dword ptr [r8 + 0x0], ecx

State #	`flag`			`mem0_value`			`r8`			`rax`			`rcx`
State #	Initial	Final	Δ	Initial	Final	Δ	Initial	Final	Δ	Initial	Final	Δ	Initial	Final	Δ
950	`—`	`0x0000000000010002`	Δ	`0x0000000000000082`	`0x0000000000000082`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x0000000000000020`	Δ	`0xFFFFFFFFFFFFFF02`	`0xFFFFFFFFFFFFFF02`	=
951	`—`	`0x0000000000010002`	Δ	`0x0000000000000082`	`0x0000000000000082`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x0000000000000082`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=
952	`—`	`0x0000000000010002`	Δ	`0x0000000000000082`	`0x0000000000000082`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x0000000000000000`	Δ	`0xFFFFFFFFFFFFFFFE`	`0xFFFFFFFFFFFFFFFE`	=
953	`—`	`0x0000000000010002`	Δ	`0x0000000000000082`	`0x0000000000000082`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x0000000000000000`	Δ	`0xFFFFFFFFFFFFFFFF`	`0xFFFFFFFFFFFFFFFF`	=
954	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFF80`	Δ	`0x0000000000000000`	`0x0000000000000000`	=
955	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFC0`	Δ	`0x0000000000000001`	`0x0000000000000001`	=
956	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFE0`	Δ	`0x0000000000000002`	`0x0000000000000002`	=
957	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFF0`	Δ	`0x0000000000000003`	`0x0000000000000003`	=
958	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0x000000000000007E`	`0x000000000000007E`	=
959	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0x000000000000007F`	`0x000000000000007F`	=
960	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFF80`	Δ	`0x0000000000000080`	`0x0000000000000080`	=
961	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFC0`	Δ	`0x0000000000000081`	`0x0000000000000081`	=
962	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFE0`	Δ	`0x0000000000000082`	`0x0000000000000082`	=
963	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0x00000000000000FD`	`0x00000000000000FD`	=
964	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0x00000000000000FE`	`0x00000000000000FE`	=
965	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0x00000000000000FF`	`0x00000000000000FF`	=
966	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFF80`	Δ	`0xFFFFFFFFFFFFFF00`	`0xFFFFFFFFFFFFFF00`	=
967	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFC0`	Δ	`0xFFFFFFFFFFFFFF01`	`0xFFFFFFFFFFFFFF01`	=
968	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFE0`	Δ	`0xFFFFFFFFFFFFFF02`	`0xFFFFFFFFFFFFFF02`	=
969	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFF80`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=
970	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0xFFFFFFFFFFFFFFFE`	`0xFFFFFFFFFFFFFFFE`	=
971	`—`	`0x0000000000010002`	Δ	`0xFFFFFFFFFFFFFF80`	`0xFFFFFFFFFFFFFF80`	=	`0x0000666666010100`	`0x0000666666010100`	=	`0xFFFFFFFFFFFFFFFF`	`0x00000000FFFFFFFF`	Δ	`0xFFFFFFFFFFFFFFFF`	`0xFFFFFFFFFFFFFFFF`	=