portugalfuturista/rizin
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
rizin/test/db/cmd/cmd_plf
Rot127 9b227eb3c1
Make AArch64/ARM analysis and asm plugins Capstone v6 compatible. (#4011) 
This commit refactors the AArch64 and partially the ARM
plugin to make it Capstone v6 compatible.
Due to the big API changes in Capstone v6 several changes
had to be made.

Because we need to be compatible to Capstone v4 and v5
many include guards are added as well.

Overview of changes done:

**ARM**

- Instruction alias were introduced. This leads to different
decoding and analysis paths taken for certain instructions.
Some alias have their IL code generated like the real
instruction now (no special handling needed anymore).
This change is responsible for many changes you'll encounter.

- The operand details of each instruction are now always the
one of the real instruction. Also for alias.
For example, if "MOV <Wd>, #<imm>" is an alias for `ORR <Wd>, WZR, #<imm>`,
the details by CS hold all three operands of "ORR".
Before, they held only the two of "MOV".

- Several bugs in variable and argument generation
were fixed. Especially the default variable width
for ARM Thumb was changed to 32bit instead of the 16bit.

**AArch64/ARM64**

The changes listed above for ARM, also apply to AArch64.

Additionally:

- Capstone v6 changed the name ARM64 now everywhere to AArch64.
To be compatible with Capstone v4/v5 AArch64 names must be wrapped
into macros which resolve the name, depending on the CS version used.

- Capstone v6 is now more consistent with
register real and alias names.
From now on we use the register alias by default.

**List squashed commit messages:**

[AArch64 CS v6 BEGIN] Change subproject config to use cs-auto-sync-aarch64 branch

Replace ARM64 with version sensitive macros.

Exclude alias if CS version >= 6

Update access to writeback member

Exclude instr alias from inclusion

Update memory operand printing to json.

Enable real instr. detail only for AArch64

Set correct arch name in meson.build for CS

Fix U/SBFM instructions and their alias.

Mark parameters with RZ_OUt/BORROW

Optimize register extension to skip some, if the width already matches.

Adapt width and lsb of U/SBFM alias instructions (ImmR and ImmS are from U/SBFM).

Fix tests correct semantic buy bad syntax

Pass alias MOV instructions to mov()

Handle CSET and CSETM alias

Fix lsl, lsr and asr by handling them as alias.

Fix mov alias.

Handle TST alias

Fix CNEG, CINV alias

Fix bfi and bfxil alias.

Fix sign extensions.

Fix compare instructions.

Fix NEG, NGC, NGCS, NEGS, MVN

Fix CINC

Fix multiply instructions.

Fix ROR

Run clang-format

Handle CMP for ESIL

Handle new position of memory disponents of post index operands.

Fix post-index operations.

Add missing writeback checks for Post and preindex

Handle UBFM and SBFM alias

Handl BFM alias

Handle CMP, CSET and CINC alias

Update meson file of for cs-aarch64 branch

Fix asm tests. Use reg alias now.

Fix condition confusion and incorrect operand usage.

Fix plf test.

Run clang-format

Use register alias in tests

Add support for fp and lr reg alias assembly.

Use reg alias in test

Rename cond tranlate functions r2 -> rz

Fix condition check which assume 0 == invalid.

Fix issues intruduced by rebase

Set CS commit to current next branch.

Rename ARM64 -> AArch64

Add missing source file to meson.build

Remove DisassemblerExtension.c file for CS v5

Update to newest capstone next branch

Bump up CS version

REVERT ME: Get Capstone v4/v5 via git clone until new tars are released.

Wrap setting of CS_DETAIL_REAL into CS version check

Add maybe-unitialized to Capstone C args.

Fix CS pre v6 build by adding guards.

Use reg alias now printed by default by CS.

Bump CS version to most recent next.

Fix build errors due to stircter alias handling in ARM.

Fix RzIL tests introduced by alias introduction to ARM.

Fix ESIL bugs introduced with ARM alias introduction.

- stackptr hasn't been set for POP and PUSH

Add support again for Thumb1 pop/push

Handle PUSHW and POPW alias

Update test case

Add more POP and PUSH alias and enrich detail for other versions of them.

Fix incorrect mem access width guesses for ARM thumb.

Set POP return info if it writes to PC

Fix tests about default var size and POP mem write direction.

Bump CS version to newest next.

Fix incorrect tests.

- TriCore: Functions were in ro section.
- Default arg width in ARM thumb is 32bit.

Revert check for a set stackptr.

stackptr is used in different ways:
1. Safes the offset from the stack frame base.
2. Is interpreted as somthing else for x86 and I cannot find out what, in a reasonably time.

Hence we cannot use it here consistently.

Remove check for non existing ARM_GRP_RET in CSv5

Fix incorrect stack offsets of variables.

'push <reg-list>' instructions for which the second register was the FP,
reset the stackptr variable to 0. This led to wrong bp offsets in the variable names.
In this case it was +0xc.

Bump CS version.

Add copy of meta-programming macros for capstone-sys build.

Update capstone-next.wrap

Use bracket-less met-programming macro to fix Windows build warnings.

Update wrap files for Capstone with branch names

Add new meta-programming macro

Add workaround for MSVC pre-processor bug.
2023-12-20 01:00:31 +08:00

815 lines
81 KiB
Text
Raw Blame History

NAME=plf
FILE=bins/elf/ls
CMDS=<<EOF
aaa
plf
echo "---"
so 1
plf
EOF
EXPECT=<<EOF
0x5ae0 empty
0x5ae4 (seq (set _xor (^ (cast 32 false (var rbp)) (cast 32 false (var rbp)))) (set rbp (cast 64 false (var _xor))) (set of false) (set cf false) (set _result (var _xor)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
0x5ae6 (set r9 (cast 64 false (var rdx)))
0x5ae9 (seq (set rsi (loadw 0 64 (+ (var rsp) (bv 64 0x0)))) (set rsp (+ (var rsp) (bv 64 0x8))))
0x5aea (set rdx (var rsp))
0x5aed (seq (set and_ (& (var rsp) (bv 64 0xfffffffffffffff0))) (set rsp (var and_)) (set of false) (set cf false) (set _result (var and_)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
0x5af1 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var rax))) (set rsp (var final)))
0x5af2 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var rsp))) (set rsp (var final)))
0x5af3 (set r8 (cast 64 false (cast 64 false (+ (bv 64 0x5afa) (bv 64 0x10c66)))))
0x5afa (set rcx (cast 64 false (+ (bv 64 0x5b01) (bv 64 0x10bef))))
0x5b01 (set rdi (cast 64 false (+ (bv 64 0x5b08) (bv 64 0xffffffffffffe568))))
0x5b08 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x5b0e))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x5b0e) (bv 64 0x1c30a)))))
---
0x5ae0 empty
0x5ae4 (seq (set _xor (^ (cast 32 false (var rbp)) (cast 32 false (var rbp)))) (set rbp (cast 64 false (var _xor))) (set of false) (set cf false) (set _result (var _xor)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
0x5ae6 (set r9 (cast 64 false (var rdx)))
0x5ae9 (seq (set rsi (loadw 0 64 (+ (var rsp) (bv 64 0x0)))) (set rsp (+ (var rsp) (bv 64 0x8))))
0x5aea (set rdx (var rsp))
0x5aed (seq (set and_ (& (var rsp) (bv 64 0xfffffffffffffff0))) (set rsp (var and_)) (set of false) (set cf false) (set _result (var and_)) (set _popcnt (bv 8 0x0)) (set _val (cast 8 false (var _result))) (repeat (! (is_zero (var _val))) (seq (set _popcnt (+ (var _popcnt) (ite (lsb (var _val)) (bv 8 0x1) (bv 8 0x0)))) (set _val (>> (var _val) (bv 8 0x1) false)))) (set pf (is_zero (mod (var _popcnt) (bv 8 0x2)))) (set zf (is_zero (var _result))) (set sf (msb (var _result))))
0x5af1 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var rax))) (set rsp (var final)))
0x5af2 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (var rsp))) (set rsp (var final)))
0x5af3 (set r8 (cast 64 false (cast 64 false (+ (bv 64 0x5afa) (bv 64 0x10c66)))))
0x5afa (set rcx (cast 64 false (+ (bv 64 0x5b01) (bv 64 0x10bef))))
0x5b01 (set rdi (cast 64 false (+ (bv 64 0x5b08) (bv 64 0xffffffffffffe568))))
0x5b08 (seq (set final (- (var rsp) (bv 64 0x8))) (storew 0 (var final) (cast 64 false (bv 64 0x5b0e))) (set rsp (var final)) (jmp (loadw 0 64 (+ (bv 64 0x5b0e) (bv 64 0x1c30a)))))
EOF
RUN
NAME=plf big function
FILE=malloc://10240
CMDS=<<EOF
. bins/arm/arm64_rzil_test.rz
aaa
plf
EOF
EXPECT=<<EOF
0x0 (set x8 (cast 64 false (load 0 (+ (var x2) (bv 64 0x104)))))
0x4 (branch (lsb (>> (cast 64 false (cast 32 false (var x8))) (bv 6 0x1) false)) (jmp (bv 64 0x10)) nop)
0x8 (set x0 (cast 64 false (bv 32 0x0)))
0xc (jmp (var x30))
0x10 (set x9 (cast 64 false (loadw 0 32 (+ (var x2) (bv 64 0x100)))))
0x14 (set x8 (cast 64 false (<< (cast 32 false (var x9)) (bv 6 0x2) false)))
0x18 (set x8 (+ (var x2) (<< (cast 64 false (cast 32 false (var x8))) (bv 6 0x2) false)))
0x1c (seq (set addr (var x0)) (set x10 (cast 64 false (loadw 0 32 (var addr)))) (set x11 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x20 (seq (set addr (var x8)) (set x12 (cast 64 false (loadw 0 32 (var addr)))) (set x13 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x24 (set x12 (cast 64 false (^ (cast 32 false (var x10)) (cast 32 false (var x12)))))
0x28 (set x13 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x13)))))
0x2c (seq (set addr (+ (var x0) (bv 64 0x8))) (set x10 (cast 64 false (loadw 0 32 (var addr)))) (set x11 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x30 (seq (set addr (+ (var x8) (bv 64 0x8))) (set x14 (cast 64 false (loadw 0 32 (var addr)))) (set x8 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x34 (set x14 (cast 64 false (^ (cast 32 false (var x10)) (cast 32 false (var x14)))))
0x38 (set x15 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x8)))))
0x3c (set x8 (bv 64 0x5fe60))
0x40 nop
0x44 (seq (set a (cast 32 false (var x9))) (set b (bv 32 0xa)) (set r (- (var a) (var b))) (set cf (ule (var b) (var a))) (set vf (&& (^^ (msb (var a)) (msb (var b))) (^^ (msb (var a)) (msb (var r))))) (set zf (is_zero (var r))) (set nf (msb (var r))))
0x48 (branch (var zf) (jmp (bv 64 0x394)) nop)
0x4c (seq (set a (cast 32 false (var x9))) (set b (bv 32 0xc)) (set r (- (var a) (var b))) (set cf (ule (var b) (var a))) (set vf (&& (^^ (msb (var a)) (msb (var b))) (^^ (msb (var a)) (msb (var r))))) (set zf (is_zero (var r))) (set nf (msb (var r))))
0x50 (branch (var zf) (jmp (bv 64 0x1f8)) nop)
0x54 (seq (set a (cast 32 false (var x9))) (set b (bv 32 0xe)) (set r (- (var a) (var b))) (set cf (ule (var b) (var a))) (set vf (&& (^^ (msb (var a)) (msb (var b))) (^^ (msb (var a)) (msb (var r))))) (set zf (is_zero (var r))) (set nf (msb (var r))))
0x58 (branch (! (var zf)) (jmp (bv 64 0xb84)) nop)
0x5c (set x9 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x60 (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0x64 (set x9 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x68 (set x11 (+ (var x8) (bv 64 0x400)))
0x6c (set x17 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0x70 (set x10 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x74 (set x9 (+ (var x8) (bv 64 0x800)))
0x78 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x10))) (bv 6 0x2) false)))))
0x7c (set x3 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x80 (set x10 (+ (var x8) (bv 64 0xc00)))
0x84 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x88 (seq (set addr (+ (var x2) (bv 64 0xd0))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x8c (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x90 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x17)))))
0x94 (set x17 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x98 (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x9c (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x0)))))
0xa0 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xa4 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0xa8 (set x0 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0xac (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xb0 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0xb4 (set x4 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0xb8 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0xbc (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x5)))))
0xc0 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x0)))))
0xc4 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x3)))))
0xc8 (set x0 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0xcc (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0xd0 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xd4 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0xd8 (seq (set addr (+ (var x2) (bv 64 0xd8))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0xdc (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0xe0 (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xe4 (set x5 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0xe8 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0xec (set x3 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0xf0 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0xf4 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0xf8 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0xfc (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x100 (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x104 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x108 (set x14 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x10c (set x13 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x110 (set x13 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x114 (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x118 (set x12 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x11c (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x120 (set x14 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x14)))))
0x124 (set x13 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x13)))))
0x128 (set x15 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x12)))))
0x12c (set x12 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x130 (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x134 (set x13 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x138 (set x13 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x13c (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x140 (set x14 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x144 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x4)))))
0x148 (set x3 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x14c (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x150 (seq (set addr (+ (var x2) (bv 64 0xc0))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x154 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x4)))))
0x158 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x13)))))
0x15c (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x14)))))
0x160 (set x13 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x164 (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x168 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x16c (set x14 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x170 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x174 (set x4 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x178 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x3)))))
0x17c (set x3 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x180 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x184 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x5)))))
0x188 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x14)))))
0x18c (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x4)))))
0x190 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x3)))))
0x194 (set x14 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x198 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x19c (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x1a0 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x1a4 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x1a8 (set x4 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x1ac (seq (set addr (+ (var x2) (bv 64 0xc8))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x1b0 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x1b4 (set x5 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x1b8 (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x1bc (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x3)))))
0x1c0 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0x1c4 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x1c8 (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x1cc (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x1d0 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x1d4 (set x11 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x1d8 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x1dc (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x1e0 (set x9 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x1e4 (set x11 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x11)))))
0x1e8 (set x9 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x9)))))
0x1ec (set x11 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x1f0 (set x10 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0x1f4 (set x15 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x10)))))
0x1f8 (set x9 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x1fc (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0x200 (set x9 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x204 (set x11 (+ (var x8) (bv 64 0x400)))
0x208 (set x17 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0x20c (set x10 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x210 (set x9 (+ (var x8) (bv 64 0x800)))
0x214 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x10))) (bv 6 0x2) false)))))
0x218 (set x3 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x21c (set x10 (+ (var x8) (bv 64 0xc00)))
0x220 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x224 (seq (set addr (+ (var x2) (bv 64 0xb0))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x228 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x22c (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x17)))))
0x230 (set x17 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x234 (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x238 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x0)))))
0x23c (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x240 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x244 (set x0 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x248 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x24c (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x250 (set x4 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x254 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x258 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x5)))))
0x25c (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x0)))))
0x260 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x3)))))
0x264 (set x0 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x268 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x26c (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x270 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x274 (seq (set addr (+ (var x2) (bv 64 0xb8))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x278 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x27c (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x280 (set x5 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x284 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x288 (set x3 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x28c (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x290 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x294 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x298 (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x29c (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x2a0 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x2a4 (set x14 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x2a8 (set x13 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x2ac (set x13 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x2b0 (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x2b4 (set x12 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x2b8 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x2bc (set x14 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x14)))))
0x2c0 (set x13 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x13)))))
0x2c4 (set x15 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x12)))))
0x2c8 (set x12 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x2cc (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x2d0 (set x13 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x2d4 (set x13 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x2d8 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x2dc (set x14 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x2e0 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x4)))))
0x2e4 (set x3 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x2e8 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x2ec (seq (set addr (+ (var x2) (bv 64 0xa0))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x2f0 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x4)))))
0x2f4 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x13)))))
0x2f8 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x14)))))
0x2fc (set x13 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x300 (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x304 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x308 (set x14 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x30c (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x310 (set x4 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x314 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x3)))))
0x318 (set x3 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x31c (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x320 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x5)))))
0x324 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x14)))))
0x328 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x4)))))
0x32c (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x3)))))
0x330 (set x14 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x334 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x338 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x33c (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x340 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x344 (set x4 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x348 (seq (set addr (+ (var x2) (bv 64 0xa8))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x34c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x350 (set x5 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x354 (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x358 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x3)))))
0x35c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0x360 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x364 (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x368 (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x36c (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x370 (set x11 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x374 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x378 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x37c (set x9 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x380 (set x11 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x11)))))
0x384 (set x9 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x9)))))
0x388 (set x11 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x38c (set x10 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0x390 (set x15 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x10)))))
0x394 (set x9 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x398 (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0x39c (set x10 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x3a0 (set x9 (+ (var x8) (bv 64 0x400)))
0x3a4 (set x17 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x10))) (bv 6 0x2) false)))))
0x3a8 (set x11 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x3ac (set x10 (+ (var x8) (bv 64 0x800)))
0x3b0 (set x0 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0x3b4 (set x3 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x3b8 (set x11 (+ (var x8) (bv 64 0xc00)))
0x3bc (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x3c0 (seq (set addr (+ (var x2) (bv 64 0x90))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x3c4 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x3c8 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x17)))))
0x3cc (set x17 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x3d0 (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x3d4 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x0)))))
0x3d8 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x3dc (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x3e0 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x3e4 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x3e8 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x3ec (set x3 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x3f0 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x3f4 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x5)))))
0x3f8 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x0)))))
0x3fc (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x4)))))
0x400 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x3)))))
0x404 (set x0 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x408 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x40c (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x410 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x414 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x418 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x41c (set x5 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x420 (set x5 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x424 (seq (set addr (+ (var x2) (bv 64 0x98))) (set x6 (cast 64 false (loadw 0 32 (var addr)))) (set x7 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x428 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x6)))))
0x42c (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x430 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x4)))))
0x434 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x438 (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x43c (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x440 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x444 (set x14 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x448 (set x13 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x44c (set x13 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x450 (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x454 (set x12 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x458 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x7)))))
0x45c (set x14 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x14)))))
0x460 (set x13 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x13)))))
0x464 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x12)))))
0x468 (set x12 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x46c (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x470 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x474 (set x14 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x478 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x47c (set x15 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x480 (set x3 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x484 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x488 (seq (set addr (+ (var x2) (bv 64 0x80))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x48c (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x4)))))
0x490 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x14)))))
0x494 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x15)))))
0x498 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x3)))))
0x49c (set x14 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x4a0 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x4a4 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x4a8 (set x15 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x4ac (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x4b0 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x4b4 (set x4 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x4b8 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x4bc (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x4c0 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x15)))))
0x4c4 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x3)))))
0x4c8 (set x15 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x4cc (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x4d0 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x4d4 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x4d8 (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x4dc (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x4e0 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0x4e4 (set x4 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x4e8 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x4ec (seq (set addr (+ (var x2) (bv 64 0x88))) (set x6 (cast 64 false (loadw 0 32 (var addr)))) (set x7 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x4f0 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x4f4 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x3)))))
0x4f8 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x5)))))
0x4fc (set x13 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x500 (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x504 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x508 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x50c (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x510 (set x17 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x514 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x4)))))
0x518 (set x16 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x51c (set x16 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x520 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x7)))))
0x524 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x0)))))
0x528 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x17)))))
0x52c (set x16 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x16)))))
0x530 (set x13 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x534 (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x538 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x53c (set x17 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x540 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x544 (set x0 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x548 (set x3 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x54c (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x550 (seq (set addr (+ (var x2) (bv 64 0x70))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x554 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x4)))))
0x558 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x17)))))
0x55c (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x0)))))
0x560 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x3)))))
0x564 (set x17 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x568 (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x56c (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x570 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x574 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x578 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x57c (set x4 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x580 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x584 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x5)))))
0x588 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x0)))))
0x58c (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x3)))))
0x590 (set x0 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x594 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x598 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x59c (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x5a0 (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x5a4 (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x5a8 (seq (set addr (+ (var x2) (bv 64 0x78))) (set x6 (cast 64 false (loadw 0 32 (var addr)))) (set x7 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x5ac (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x6)))))
0x5b0 (set x6 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x5b4 (set x6 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x6))) (bv 6 0x2) false)))))
0x5b8 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x5bc (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x5c0 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x6)))))
0x5c4 (set x16 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x5c8 (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x5cc (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x5d0 (set x15 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x5d4 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x5d8 (set x14 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x5dc (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x5e0 (set x12 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x5e4 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x7)))))
0x5e8 (set x15 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x15)))))
0x5ec (set x14 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x14)))))
0x5f0 (set x12 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x12)))))
0x5f4 (set x14 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x5f8 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x5fc (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x600 (set x15 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x604 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x608 (set x16 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x60c (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x4)))))
0x610 (set x3 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x614 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x618 (seq (set addr (+ (var x2) (bv 64 0x60))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x61c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0x620 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x15)))))
0x624 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x16)))))
0x628 (set x15 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x62c (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x630 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x634 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x638 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x63c (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x640 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x3)))))
0x644 (set x3 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x648 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x64c (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x5)))))
0x650 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x16)))))
0x654 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x4)))))
0x658 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x3)))))
0x65c (set x16 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x660 (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x664 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x668 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x66c (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x670 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x674 (set x5 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x678 (set x5 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x67c (seq (set addr (+ (var x2) (bv 64 0x68))) (set x6 (cast 64 false (loadw 0 32 (var addr)))) (set x7 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x680 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x6)))))
0x684 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x688 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x68c (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x690 (set x12 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x694 (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x698 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x69c (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x6a0 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x6a4 (set x17 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x6a8 (set x13 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x6ac (set x13 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x6b0 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x7)))))
0x6b4 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x0)))))
0x6b8 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x17)))))
0x6bc (set x13 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x13)))))
0x6c0 (set x12 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x6c4 (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x6c8 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x6cc (set x17 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x6d0 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x6d4 (set x0 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x6d8 (set x3 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x6dc (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x6e0 (seq (set addr (+ (var x2) (bv 64 0x50))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x6e4 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x4)))))
0x6e8 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x17)))))
0x6ec (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x0)))))
0x6f0 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x3)))))
0x6f4 (set x17 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x6f8 (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x6fc (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x700 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x704 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x708 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x70c (set x4 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x710 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x714 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x5)))))
0x718 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x0)))))
0x71c (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x3)))))
0x720 (set x0 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x724 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x728 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x72c (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x730 (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x734 (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x738 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x4)))))
0x73c (set x4 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x740 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x744 (seq (set addr (+ (var x2) (bv 64 0x58))) (set x6 (cast 64 false (loadw 0 32 (var addr)))) (set x7 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x748 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x6)))))
0x74c (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x750 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x754 (set x13 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x758 (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x75c (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x760 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x764 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x768 (set x15 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x76c (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x4)))))
0x770 (set x14 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x774 (set x14 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x778 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x7)))))
0x77c (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x16)))))
0x780 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x15)))))
0x784 (set x14 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x14)))))
0x788 (set x13 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x78c (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x790 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x794 (set x15 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x798 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x79c (set x16 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x7a0 (set x3 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x7a4 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x7a8 (seq (set addr (+ (var x2) (bv 64 0x40))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x7ac (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x4)))))
0x7b0 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x15)))))
0x7b4 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x16)))))
0x7b8 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x3)))))
0x7bc (set x15 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x7c0 (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x7c4 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x7c8 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x7cc (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x7d0 (set x3 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x7d4 (set x4 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x7d8 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x7dc (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x5)))))
0x7e0 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x16)))))
0x7e4 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x3)))))
0x7e8 (set x16 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x7ec (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x7f0 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x7f4 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x7f8 (seq (set addr (+ (var x2) (bv 64 0x48))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x7fc (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x800 (set x5 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x804 (set x5 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x808 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x80c (set x3 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x810 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x814 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x818 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x81c (set x14 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x820 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x824 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x828 (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x82c (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x830 (set x17 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x834 (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x838 (set x12 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x83c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x6)))))
0x840 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x0)))))
0x844 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x17)))))
0x848 (set x17 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x12)))))
0x84c (set x12 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x850 (set x12 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x854 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x858 (set x14 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x85c (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x860 (set x0 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x864 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x4)))))
0x868 (set x3 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x86c (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x870 (seq (set addr (+ (var x2) (bv 64 0x30))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x874 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x4)))))
0x878 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x14)))))
0x87c (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x0)))))
0x880 (set x14 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x884 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x888 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x88c (set x0 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x890 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x894 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x898 (set x12 (cast 64 false (^ (cast 32 false (var x12)) (cast 32 false (var x3)))))
0x89c (set x3 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0x8a0 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x8a4 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0x8a8 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x0)))))
0x8ac (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0x8b0 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x3)))))
0x8b4 (set x0 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0x8b8 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0x8bc (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x8c0 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x8c4 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x8c8 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x8cc (seq (set addr (+ (var x2) (bv 64 0x38))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x8d0 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x8d4 (set x5 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x8d8 (set x5 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x8dc (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x3)))))
0x8e0 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x4)))))
0x8e4 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0x8e8 (set x17 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0x8ec (set x17 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x8f0 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x8f4 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x8f8 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x8fc (set x15 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x900 (set x13 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0x904 (set x13 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x908 (set x17 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x6)))))
0x90c (set x16 (cast 64 false (^ (cast 32 false (var x17)) (cast 32 false (var x16)))))
0x910 (set x15 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x15)))))
0x914 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x13)))))
0x918 (set x13 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0x91c (set x13 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0x920 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x924 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x928 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x92c (set x17 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x930 (set x3 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0x934 (set x3 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x938 (seq (set addr (+ (var x2) (bv 64 0x20))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x93c (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x4)))))
0x940 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x16)))))
0x944 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x17)))))
0x948 (set x16 (cast 64 false (& (cast 32 false (var x14)) (bv 32 0xff))))
0x94c (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x950 (set x17 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x954 (set x17 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x17))) (bv 6 0x2) false)))))
0x958 (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x95c (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x960 (set x6 (cast 64 false (>> (cast 32 false (var x0)) (bv 6 0x18) false)))
0x964 (set x6 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x6))) (bv 6 0x2) false)))))
0x968 (set x13 (cast 64 false (^ (cast 32 false (var x13)) (cast 32 false (var x3)))))
0x96c (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x970 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x17)))))
0x974 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x978 (set x17 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x6)))))
0x97c (set x16 (cast 64 false (& (cast 32 false (var x0)) (bv 32 0xff))))
0x980 (set x16 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x984 (set x3 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x988 (set x3 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x3))) (bv 6 0x2) false)))))
0x98c (set x4 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x990 (set x4 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0x994 (seq (set addr (+ (var x2) (bv 64 0x28))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0x998 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x99c (set x5 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0x9a0 (set x5 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0x9a4 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x3)))))
0x9a8 (set x16 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x4)))))
0x9ac (set x3 (cast 64 false (^ (cast 32 false (var x16)) (cast 32 false (var x5)))))
0x9b0 (set x15 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0x9b4 (set x15 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x9b8 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x0)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x9bc (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x9c0 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x9c4 (set x14 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x9c8 (set x12 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0x9cc (set x12 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0x9d0 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x6)))))
0x9d4 (set x15 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x16)))))
0x9d8 (set x14 (cast 64 false (^ (cast 32 false (var x15)) (cast 32 false (var x14)))))
0x9dc (set x12 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x12)))))
0x9e0 (set x14 (cast 64 false (& (cast 32 false (var x13)) (bv 32 0xff))))
0x9e4 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0x9e8 (set x15 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0x9ec (set x15 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x15))) (bv 6 0x2) false)))))
0x9f0 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x3)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0x9f4 (set x16 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0x9f8 (set x0 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0x9fc (set x0 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0xa00 (seq (set addr (+ (var x2) (bv 64 0x10))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0xa04 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0xa08 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x15)))))
0xa0c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x16)))))
0xa10 (set x15 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x0)))))
0xa14 (set x14 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0xa18 (set x14 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0xa1c (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xa20 (set x16 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0xa24 (set x0 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xa28 (set x0 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x0))) (bv 6 0x2) false)))))
0xa2c (set x4 (cast 64 false (>> (cast 32 false (var x3)) (bv 6 0x18) false)))
0xa30 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0xa34 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x5)))))
0xa38 (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x16)))))
0xa3c (set x14 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x0)))))
0xa40 (set x16 (cast 64 false (& (cast 32 false (var x3)) (bv 32 0xff))))
0xa44 (set x0 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0xa48 (set x16 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xa4c (set x5 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x16))) (bv 6 0x2) false)))))
0xa50 (set x16 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0xa54 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xa58 (set x14 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0xa5c (seq (set addr (+ (var x2) (bv 64 0x18))) (set x4 (cast 64 false (loadw 0 32 (var addr)))) (set x6 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0xa60 (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x4)))))
0xa64 (set x4 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0xa68 (set x4 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x4))) (bv 6 0x2) false)))))
0xa6c (set x0 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x5)))))
0xa70 (set x14 (cast 64 false (^ (cast 32 false (var x0)) (cast 32 false (var x14)))))
0xa74 (set x12 (cast 64 false (& (cast 32 false (var x12)) (bv 32 0xff))))
0xa78 (set x8 (cast 64 false (loadw 0 32 (+ (var x8) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xa7c (set x12 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x3)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xa80 (set x9 (cast 64 false (loadw 0 32 (+ (var x9) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xa84 (set x12 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xa88 (set x10 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xa8c (set x12 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0xa90 (set x11 (cast 64 false (loadw 0 32 (+ (var x11) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xa94 (set x17 (cast 64 false (^ (cast 32 false (var x14)) (cast 32 false (var x4)))))
0xa98 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x6)))))
0xa9c (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x9)))))
0xaa0 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x10)))))
0xaa4 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x11)))))
0xaa8 (set x9 (cast 64 false (& (cast 32 false (var x15)) (bv 32 0xff))))
0xaac (set x10 (bv 64 0x603f0))
0xab0 nop
0xab4 (set x9 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0xab8 (set x11 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x8)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xabc (set x0 (+ (var x10) (bv 64 0x400)))
0xac0 (set x11 (cast 64 false (loadw 0 32 (+ (var x0) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0xac4 (set x12 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xac8 (set x3 (+ (var x10) (bv 64 0x800)))
0xacc (set x12 (cast 64 false (loadw 0 32 (+ (var x3) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xad0 (set x13 (cast 64 false (>> (cast 32 false (var x16)) (bv 6 0x18) false)))
0xad4 (set x4 (+ (var x10) (bv 64 0xc00)))
0xad8 (set x13 (cast 64 false (loadw 0 32 (+ (var x4) (<< (cast 64 false (cast 32 false (var x13))) (bv 6 0x2) false)))))
0xadc (seq (set addr (var x2)) (set x14 (cast 64 false (loadw 0 32 (var addr)))) (set x5 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0xae0 (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x14)))))
0xae4 (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x11)))))
0xae8 (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x12)))))
0xaec (set x11 (cast 64 false (& (cast 32 false (var x16)) (bv 32 0xff))))
0xaf0 (set x11 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0xaf4 (set x12 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xaf8 (set x14 (cast 64 false (loadw 0 32 (+ (var x0) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xafc (set x12 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x8)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xb00 (set x6 (cast 64 false (loadw 0 32 (+ (var x3) (<< (cast 64 false (cast 32 false (var x12))) (bv 6 0x2) false)))))
0xb04 (set x12 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x13)))))
0xb08 (set x9 (cast 64 false (>> (cast 32 false (var x17)) (bv 6 0x18) false)))
0xb0c (set x9 (cast 64 false (loadw 0 32 (+ (var x4) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0xb10 (set x11 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x5)))))
0xb14 (set x11 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x14)))))
0xb18 (set x11 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x6)))))
0xb1c (set x13 (cast 64 false (^ (cast 32 false (var x11)) (cast 32 false (var x9)))))
0xb20 (set x9 (cast 64 false (& (cast 32 false (var x17)) (bv 32 0xff))))
0xb24 (set x9 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0xb28 (set x11 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xb2c (set x11 (cast 64 false (loadw 0 32 (+ (var x0) (<< (cast 64 false (cast 32 false (var x11))) (bv 6 0x2) false)))))
0xb30 (set x14 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xb34 (set x14 (cast 64 false (loadw 0 32 (+ (var x3) (<< (cast 64 false (cast 32 false (var x14))) (bv 6 0x2) false)))))
0xb38 (seq (set addr (+ (var x2) (bv 64 0x8))) (set x5 (cast 64 false (loadw 0 32 (var addr)))) (set x2 (cast 64 false (loadw 0 32 (+ (var addr) (bv 64 0x4))))))
0xb3c (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x5)))))
0xb40 (set x5 (cast 64 false (>> (cast 32 false (var x8)) (bv 6 0x18) false)))
0xb44 (set x5 (cast 64 false (loadw 0 32 (+ (var x4) (<< (cast 64 false (cast 32 false (var x5))) (bv 6 0x2) false)))))
0xb48 (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x11)))))
0xb4c (set x9 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x14)))))
0xb50 (set x14 (cast 64 false (^ (cast 32 false (var x9)) (cast 32 false (var x5)))))
0xb54 (set x8 (cast 64 false (& (cast 32 false (var x8)) (bv 32 0xff))))
0xb58 (set x8 (cast 64 false (loadw 0 32 (+ (var x10) (<< (cast 64 false (cast 32 false (var x8))) (bv 6 0x2) false)))))
0xb5c (set x9 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x17)) (bv 6 0x8) false)) (cast 32 false (var res)))))
0xb60 (set x9 (cast 64 false (loadw 0 32 (+ (var x0) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0xb64 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x2)))))
0xb68 (set x10 (cast 64 false (let res (cast 8 false (>> (cast 32 false (var x16)) (bv 6 0x10) false)) (cast 32 false (var res)))))
0xb6c (set x10 (cast 64 false (loadw 0 32 (+ (var x3) (<< (cast 64 false (cast 32 false (var x10))) (bv 6 0x2) false)))))
0xb70 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x9)))))
0xb74 (set x8 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x10)))))
0xb78 (set x9 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0xb7c (set x9 (cast 64 false (loadw 0 32 (+ (var x4) (<< (cast 64 false (cast 32 false (var x9))) (bv 6 0x2) false)))))
0xb80 (set x15 (cast 64 false (^ (cast 32 false (var x8)) (cast 32 false (var x9)))))
0xb84 (store 0 (var x1) (cast 8 false (var x12)))
0xb88 (set x8 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x8) false)))
0xb8c (store 0 (+ (var x1) (bv 64 0x1)) (cast 8 false (var x8)))
0xb90 (set x8 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x10) false)))
0xb94 (store 0 (+ (var x1) (bv 64 0x2)) (cast 8 false (var x8)))
0xb98 (set x8 (cast 64 false (>> (cast 32 false (var x12)) (bv 6 0x18) false)))
0xb9c (store 0 (+ (var x1) (bv 64 0x3)) (cast 8 false (var x8)))
0xba0 (store 0 (+ (var x1) (bv 64 0x4)) (cast 8 false (var x13)))
0xba4 (set x8 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x8) false)))
0xba8 (store 0 (+ (var x1) (bv 64 0x5)) (cast 8 false (var x8)))
0xbac (set x8 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x10) false)))
0xbb0 (store 0 (+ (var x1) (bv 64 0x6)) (cast 8 false (var x8)))
0xbb4 (set x8 (cast 64 false (>> (cast 32 false (var x13)) (bv 6 0x18) false)))
0xbb8 (store 0 (+ (var x1) (bv 64 0x7)) (cast 8 false (var x8)))
0xbbc (store 0 (+ (var x1) (bv 64 0x8)) (cast 8 false (var x14)))
0xbc0 (set x8 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x8) false)))
0xbc4 (store 0 (+ (var x1) (bv 64 0x9)) (cast 8 false (var x8)))
0xbc8 (set x8 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x10) false)))
0xbcc (store 0 (+ (var x1) (bv 64 0xa)) (cast 8 false (var x8)))
0xbd0 (set x8 (cast 64 false (>> (cast 32 false (var x14)) (bv 6 0x18) false)))
0xbd4 (store 0 (+ (var x1) (bv 64 0xb)) (cast 8 false (var x8)))
0xbd8 (store 0 (+ (var x1) (bv 64 0xc)) (cast 8 false (var x15)))
0xbdc (set x8 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x8) false)))
0xbe0 (store 0 (+ (var x1) (bv 64 0xd)) (cast 8 false (var x8)))
0xbe4 (set x8 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x10) false)))
0xbe8 (store 0 (+ (var x1) (bv 64 0xe)) (cast 8 false (var x8)))
0xbec (set x8 (cast 64 false (>> (cast 32 false (var x15)) (bv 6 0x18) false)))
0xbf0 (set x0 (cast 64 false (bv 32 0x1)))
0xbf4 (store 0 (+ (var x1) (bv 64 0xf)) (cast 8 false (var x8)))
0xbf8 (jmp (var x30))
EOF
RUN
Reference in a new issue View git blame Copy permalink