d "add.w #0x1111,r1" 79111111 0x0 (seq (set _0 (bv 16 0x1111)) (set _1 (var r1)) (set r1 (+ (var _0) (var _1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (var _0) (bv 16 0xfff)) (+ (& (var _1) (bv 16 0xfff)) (ite false (bv 16 0x1) (bv 16 0x0)))) (bv 16 0x1000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 32 false (var _0)) (+ (cast 32 false (var _1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (+ (cast 32 false (var _0)) (+ (cast 32 false (var _1)) (ite false (bv 32 0x1) (bv 32 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 32 false (var _0)) (+ (cast 32 false (var _1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (! (^^ (msb (var _0)) (msb (var _1)))) (^^ (msb (var _0)) (! (is_zero (& (+ (cast 32 false (var _0)) (+ (cast 32 false (var _1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "add.l #0x1,er1" 7a1100000001 0x0 (seq (set _0 (bv 32 0x1)) (set _1 (append (var e1) (var r1))) (set e1 (cast 16 false (>> (+ (var _0) (var _1)) (bv 8 0x10) false))) (set r1 (cast 16 false (+ (var _0) (var _1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (var _0) (bv 32 0xfffffff)) (+ (& (var _1) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x100000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (! (^^ (msb (var _0)) (msb (var _1)))) (^^ (msb (var _0)) (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "add.l er1,er2" 0a92 0x0 (seq (set _0 (append (var e1) (var r1))) (set _1 (append (var e2) (var r2))) (set e2 (cast 16 false (>> (+ (var _0) (var _1)) (bv 8 0x10) false))) (set r2 (cast 16 false (+ (var _0) (var _1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (var _0) (bv 32 0xfffffff)) (+ (& (var _1) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x100000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (! (^^ (msb (var _0)) (msb (var _1)))) (^^ (msb (var _0)) (! (is_zero (& (+ (cast 64 false (var _0)) (+ (cast 64 false (var _1)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "and.w #0x1111,r1" 79611111 0x0 (seq (set _res (& (bv 16 0x1111) (var r1))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "and.w r1,r2" 6612 0x0 (seq (set _res (& (var r1) (var r2))) (set r2 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "and.l #0x11111111,er7" 7a6711111111 0x0 (seq (set _res (& (bv 32 0x11111111) (append (var e7) (var r7)))) (set e7 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r7 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "and.l er1,er2" 01f06612 0x0 (seq (set _res (& (append (var e1) (var r1)) (append (var e2) (var r2)))) (set e2 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r2 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "bra .+4369" 58001111 0x0 (jmp (bv 24 0x1115))
d "brn .+4369" 58101111 0x0 nop
d "bhi .+4369" 58201111 0x0 (branch (! (|| (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (jmp (bv 24 0x1115)) nop)
d "bls .+4369" 58301111 0x0 (branch (|| (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "bcc .+4369" 58401111 0x0 (branch (! (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "bcs .+4369" 58501111 0x0 (branch (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (jmp (bv 24 0x1115)) nop)
d "bne .+4369" 58601111 0x0 (branch (! (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "beq .+4369" 58701111 0x0 (branch (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (jmp (bv 24 0x1115)) nop)
d "bvc .+4369" 58801111 0x0 (branch (! (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "bvs .+4369" 58901111 0x0 (branch (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (jmp (bv 24 0x1115)) nop)
d "bpl .+4369" 58a01111 0x0 (branch (! (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "bmi .+4369" 58b01111 0x0 (branch (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (jmp (bv 24 0x1115)) nop)
d "bge .+4369" 58c01111 0x0 (branch (! (^^ (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (jmp (bv 24 0x1115)) nop)
d "blt .+4369" 58d01111 0x0 (branch (^^ (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))) (jmp (bv 24 0x1115)) nop)
d "bgt .+4369" 58e01111 0x0 (branch (! (|| (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (^^ (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false))))))) (jmp (bv 24 0x1115)) nop)
d "ble .+4369" 58f01111 0x0 (branch (|| (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (^^ (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (jmp (bv 24 0x1115)) nop)
d "cmp.w r5,r4" 1d54 0x0 (seq (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (var r4) (bv 16 0xfff)) (+ (& (var r5) (bv 16 0xfff)) (ite false (bv 16 0x1) (bv 16 0x0)))) (bv 16 0x1000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 32 (msb (var r4)) (var r4)) (+ (cast 32 (msb (var r5)) (var r5)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 32 (msb (var r4)) (var r4)) (+ (cast 32 (msb (var r5)) (var r5)) (ite false (bv 32 0x1) (bv 32 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (ule (var r4) (var r5)) (! (== (var r4) (var r5)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (var r4)) (msb (var r5))) (^^ (msb (var r4)) (! (is_zero (& (- (cast 32 (msb (var r4)) (var r4)) (+ (cast 32 (msb (var r5)) (var r5)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "cmp.w #0x1111,r1" 79211111 0x0 (seq (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (var r1) (bv 16 0xfff)) (+ (& (bv 16 0x1111) (bv 16 0xfff)) (ite false (bv 16 0x1) (bv 16 0x0)))) (bv 16 0x1000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 32 (msb (var r1)) (var r1)) (+ (cast 32 (msb (bv 16 0x1111)) (bv 16 0x1111)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 32 (msb (var r1)) (var r1)) (+ (cast 32 (msb (bv 16 0x1111)) (bv 16 0x1111)) (ite false (bv 32 0x1) (bv 32 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (ule (var r1) (bv 16 0x1111)) (! (== (var r1) (bv 16 0x1111)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (var r1)) (msb (bv 16 0x1111))) (^^ (msb (var r1)) (! (is_zero (& (- (cast 32 (msb (var r1)) (var r1)) (+ (cast 32 (msb (bv 16 0x1111)) (bv 16 0x1111)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "cmp.l #0x11111111,er1" 7a2111111111 0x0 (seq (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (append (var e1) (var r1)) (bv 32 0xfffffff)) (+ (& (bv 32 0x11111111) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (+ (cast 64 (msb (bv 32 0x11111111)) (bv 32 0x11111111)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (+ (cast 64 (msb (bv 32 0x11111111)) (bv 32 0x11111111)) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (ule (append (var e1) (var r1)) (bv 32 0x11111111)) (! (== (append (var e1) (var r1)) (bv 32 0x11111111)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (append (var e1) (var r1))) (msb (bv 32 0x11111111))) (^^ (msb (append (var e1) (var r1))) (! (is_zero (& (- (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (+ (cast 64 (msb (bv 32 0x11111111)) (bv 32 0x11111111)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "cmp.l er1,er2" 1f92 0x0 (seq (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (+ (& (append (var e2) (var r2)) (bv 32 0xfffffff)) (+ (& (append (var e1) (var r1)) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 64 (msb (append (var e2) (var r2))) (append (var e2) (var r2))) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 64 (msb (append (var e2) (var r2))) (append (var e2) (var r2))) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (ule (append (var e2) (var r2)) (append (var e1) (var r1))) (! (== (append (var e2) (var r2)) (append (var e1) (var r1))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (append (var e2) (var r2))) (msb (append (var e1) (var r1)))) (^^ (msb (append (var e2) (var r2))) (! (is_zero (& (- (cast 64 (msb (append (var e2) (var r2))) (append (var e2) (var r2))) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "dec.w #0x1,r1" 1b51 0x0 (seq (set _prev (var r1)) (set _res (- (var r1) (bv 16 0x1))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (sle (var _prev) (bv 16 0x8001)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "dec.w #0x2,r1" 1bd1 0x0 (seq (set _prev (var r1)) (set _res (- (var r1) (bv 16 0x2))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (sle (var _prev) (bv 16 0x8001)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "dec.l #0x1,er1" 1b71 0x0 (seq (set _prev (append (var e1) (var r1))) (set _res (- (append (var e1) (var r1)) (bv 32 0x1))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (sle (var _prev) (bv 32 0x80000001)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "dec.l #0x2,er1" 1bf1 0x0 (seq (set _prev (append (var e1) (var r1))) (set _res (- (append (var e1) (var r1)) (bv 32 0x2))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (sle (var _prev) (bv 32 0x80000001)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "inc.w #0x1,r1" 0b51 0x0 (seq (set _prev (var r1)) (set _res (+ (var r1) (bv 16 0x1))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (|| (! (sle (var _prev) (bv 16 0x7ffe))) (== (var _prev) (bv 16 0x7ffe))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "inc.w #0x2,r1" 0bd1 0x0 (seq (set _prev (var r1)) (set _res (+ (var r1) (bv 16 0x2))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (|| (! (sle (var _prev) (bv 16 0x7ffe))) (== (var _prev) (bv 16 0x7ffe))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "inc.l #0x1,er1" 0b71 0x0 (seq (set _prev (append (var e1) (var r1))) (set _res (+ (append (var e1) (var r1)) (bv 32 0x1))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (|| (! (sle (var _prev) (bv 32 0x7ffffffe))) (== (var _prev) (bv 32 0x7ffffffe))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "inc.l #0x2,er1" 0bf1 0x0 (seq (set _prev (append (var e1) (var r1))) (set _res (+ (append (var e1) (var r1)) (bv 32 0x2))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (|| (! (sle (var _prev) (bv 32 0x7ffffffe))) (== (var _prev) (bv 32 0x7ffffffe))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "divxu.w r1,er2" 5312 0x0 (seq (set quotient (cast 16 false (div (append (var e2) (var r2)) (cast 32 false (var r1))))) (set remainder (cast 16 false (mod (append (var e2) (var r2)) (cast 32 false (var r1))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var r1) (bv 16 0x0)) (! (== (var r1) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set e2 (cast 16 false (>> (append (var remainder) (var quotient)) (bv 8 0x10) false))) (set r2 (cast 16 false (append (var remainder) (var quotient)))))
d "divxs.b r1h,r2" 01d05112 0x0 (seq (set quotient (cast 8 (msb (sdiv (var r2) (cast 16 (msb (cast 8 false (>> (var r1) (bv 8 0x8) false))) (cast 8 false (>> (var r1) (bv 8 0x8) false))))) (sdiv (var r2) (cast 16 (msb (cast 8 false (>> (var r1) (bv 8 0x8) false))) (cast 8 false (>> (var r1) (bv 8 0x8) false)))))) (set remainder (cast 8 (msb (smod (var r2) (cast 16 (msb (cast 8 false (>> (var r1) (bv 8 0x8) false))) (cast 8 false (>> (var r1) (bv 8 0x8) false))))) (smod (var r2) (cast 16 (msb (cast 8 false (>> (var r1) (bv 8 0x8) false))) (cast 8 false (>> (var r1) (bv 8 0x8) false)))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r1) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set r2 (append (var remainder) (var quotient))))
d "divxs.w r1,er2" 01d05312 0x0 (seq (set quotient (cast 16 (msb (sdiv (append (var e2) (var r2)) (cast 32 (msb (var r1)) (var r1)))) (sdiv (append (var e2) (var r2)) (cast 32 (msb (var r1)) (var r1))))) (set remainder (cast 16 (msb (smod (append (var e2) (var r2)) (cast 32 (msb (var r1)) (var r1)))) (smod (append (var e2) (var r2)) (cast 32 (msb (var r1)) (var r1))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var r1) (bv 16 0x0)) (! (== (var r1) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set e2 (cast 16 false (>> (append (var remainder) (var quotient)) (bv 8 0x10) false))) (set r2 (cast 16 false (append (var remainder) (var quotient)))))
d "eepmov.w" 7bd4598f 0x0 (repeat (! (== (var r4) (bv 16 0x0))) (seq (set data_val (loadw 0 16 (cast 24 false (append (var e5) (var r5))))) (storew 0 (cast 24 false (append (var e6) (var r6))) (var data_val)) (set e5 (cast 16 false (>> (+ (append (var e5) (var r5)) (bv 32 0x2)) (bv 8 0x10) false))) (set r5 (cast 16 false (+ (append (var e5) (var r5)) (bv 32 0x2)))) (set e6 (cast 16 false (>> (+ (append (var e6) (var r6)) (bv 32 0x2)) (bv 8 0x10) false))) (set r6 (cast 16 false (+ (append (var e6) (var r6)) (bv 32 0x2)))) (set r4 (- (var r4) (bv 16 0x1)))))
d "exts.w r0" 17d0 0x0 (seq (set val (cast 16 false (>> (cast 32 false (<< (cast 32 false (var r0)) (- (- (bv 32 0x20) (bv 32 0x8)) (bv 32 0x8)) false)) (- (bv 32 0x20) (bv 32 0x8)) (msb (cast 32 false (<< (cast 32 false (var r0)) (- (- (bv 32 0x20) (bv 32 0x8)) (bv 32 0x8)) false)))))) (set r0 (var val)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var val) (bv 16 0x0)) (! (== (var val) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var val)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "exts.l er0" 17f0 0x0 (seq (set val (cast 32 false (>> (cast 32 false (<< (cast 32 false (append (var e0) (var r0))) (- (- (bv 32 0x20) (bv 32 0x10)) (bv 32 0x10)) false)) (- (bv 32 0x20) (bv 32 0x10)) (msb (cast 32 false (<< (cast 32 false (append (var e0) (var r0))) (- (- (bv 32 0x20) (bv 32 0x10)) (bv 32 0x10)) false)))))) (set e0 (cast 16 false (>> (var val) (bv 8 0x10) false))) (set r0 (cast 16 false (var val))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var val) (bv 32 0x0)) (! (== (var val) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var val)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "extu.w r0" 1750 0x0 (seq (set val (& (var r0) (bv 16 0xff))) (set r0 (var val)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var val)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "extu.l er0" 1770 0x0 (seq (set val (& (append (var e0) (var r0)) (bv 32 0xffff))) (set e0 (cast 16 false (>> (var val) (bv 8 0x10) false))) (set r0 (cast 16 false (var val))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var val)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "ldc.w @er1,ccr" 01406910 0x0 (set ccr (loadw 0 8 (cast 24 false (append (var e1) (var r1)))))
d "ldc.w @(+4369,er1),ccr" 01406f101111 0x0 (set ccr (loadw 0 8 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x1111)))))
d "ldc.w @(+1118481,er1),ccr" 014078106b2000111111 0x0 (set ccr (loadw 0 8 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111)))))
d "ldc.w @er1+,ccr" 01406d10 0x0 (seq (set ccr (load 0 (cast 24 false (append (var e1) (var r1))))) (set e1 (cast 16 false (>> (+ (append (var e1) (var r1)) (bv 32 0x2)) (bv 8 0x10) false))) (set r1 (cast 16 false (+ (append (var e1) (var r1)) (bv 32 0x2)))))
d "ldc.w @0x1111,ccr" 01406b001111 0x0 (set ccr (loadw 0 8 (bv 24 0x1111)))
d "ldc.w @0x111111,ccr" 01406b2000111111 0x0 (set ccr (loadw 0 8 (bv 24 0x111111)))
d "mov.b @(-27500,er3),r6h" 6e369494 0x0 (seq (set r6 (cast 16 false (| (& (cast 32 false (var r6)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (bv 32 0x8) false))) (& (<< (cast 32 false (loadw 0 8 (cast 24 false (+ (append (var e3) (var r3)) (bv 32 0xffff9494))))) (bv 32 0x8) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (bv 32 0x8) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (loadw 0 8 (cast 24 false (+ (append (var e3) (var r3)) (bv 32 0xffff9494)))) (bv 8 0x0)) (! (== (loadw 0 8 (cast 24 false (+ (append (var e3) (var r3)) (bv 32 0xffff9494)))) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (loadw 0 8 (cast 24 false (+ (append (var e3) (var r3)) (bv 32 0xffff9494))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r2l,@(+4369,er2)" 6eaa1111 0x0 (seq (storew 0 (cast 24 false (+ (append (var e2) (var r2)) (bv 32 0x1111))) (cast 8 false (var r2))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (var r2)) (bv 8 0x0)) (! (== (cast 8 false (var r2)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (var r2))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r2h,@er1" 6892 0x0 (seq (storew 0 (cast 24 false (append (var e1) (var r1))) (cast 8 false (>> (var r2) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r2) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r2h,@(+4369,er1)" 6e921111 0x0 (seq (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x1111))) (cast 8 false (>> (var r2) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r2) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r2h,@(+1118481,er1)" 78106aa200111111 0x0 (seq (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111))) (cast 8 false (>> (var r2) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r2) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r2h,@-er1" 6c92 0x0 (seq (set e1 (cast 16 false (>> (- (append (var e1) (var r1)) (bv 32 0x1)) (bv 8 0x10) false))) (set r1 (cast 16 false (- (append (var e1) (var r1)) (bv 32 0x1)))) (store 0 (cast 24 false (append (var e1) (var r1))) (cast 8 false (>> (var r2) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r2) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r2) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r1h,@0xffff11" 3111 0x0 (seq (storew 0 (bv 24 0xffff11) (cast 8 false (>> (var r1) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r1) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r1h,@0x1111" 6a811111 0x0 (seq (storew 0 (bv 24 0x1111) (cast 8 false (>> (var r1) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r1) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.b r1h,@0x111111" 6aa100111111 0x0 (seq (storew 0 (bv 24 0x111111) (cast 8 false (>> (var r1) (bv 8 0x8) false))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)) (! (== (cast 8 false (>> (var r1) (bv 8 0x8) false)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (>> (var r1) (bv 8 0x8) false))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.w @(+30481,er7),r4" 6f747711 0x0 (seq (set data_value (loadw 0 16 (cast 24 false (+ (append (var e7) (var r7)) (bv 32 0x7711))))) (set r4 (var data_value)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 16 0x0)) (! (== (var data_value) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.w r4,@(+257,er3)" 6fb40101 0x0 (seq (storew 0 (cast 24 false (+ (append (var e3) (var r3)) (bv 32 0x101))) (var r4)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var r4) (bv 16 0x0)) (! (== (var r4) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var r4)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.w @(+1118481,er1),r2" 78106b2200111111 0x0 (seq (set data_value (loadw 0 16 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111))))) (set r2 (var data_value)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 16 0x0)) (! (== (var data_value) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.w @0x111111,r1" 6b2100111111 0x0 (seq (set data_value (loadw 0 16 (bv 24 0x111111))) (set r1 (var data_value)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 16 0x0)) (! (== (var data_value) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er1,er2" 0f92 0x0 (seq (set data_value (append (var e1) (var r1))) (set e2 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r2 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l #0x11111111,er1" 7a0111111111 0x0 (seq (set e1 (cast 16 false (>> (bv 32 0x11111111) (bv 8 0x10) false))) (set r1 (cast 16 false (bv 32 0x11111111))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (bv 32 0x11111111) (bv 32 0x0)) (! (== (bv 32 0x11111111) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (bv 32 0x11111111)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @er1,er2" 01006912 0x0 (seq (set data_value (loadw 0 32 (cast 24 false (append (var e1) (var r1))))) (set e2 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r2 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @(+4369,er1),er2" 01006f121111 0x0 (seq (set data_value (loadw 0 32 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x1111))))) (set e2 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r2 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @(+1118481,er1),er2" 010078106b2200111111 0x0 (seq (set data_value (loadw 0 32 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111))))) (set e2 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r2 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @er1+,er2" 01006d12 0x0 (seq (set data_value (loadw 0 32 (cast 24 false (append (var e1) (var r1))))) (set e2 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r2 (cast 16 false (var data_value))) (set e1 (cast 16 false (>> (+ (append (var e1) (var r1)) (bv 32 0x4)) (bv 8 0x10) false))) (set r1 (cast 16 false (+ (append (var e1) (var r1)) (bv 32 0x4)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @0x1111,er1" 01006b011111 0x0 (seq (set data_value (loadw 0 32 (bv 24 0x1111))) (set e1 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r1 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @0xff8111,er1" 01006b018111 0x0 (seq (set data_value (loadw 0 32 (bv 24 0xff8111))) (set e1 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r1 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l @0x111111,er1" 01006b2100111111 0x0 (seq (set data_value (loadw 0 32 (bv 24 0x111111))) (set e1 (cast 16 false (>> (var data_value) (bv 8 0x10) false))) (set r1 (cast 16 false (var data_value))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var data_value) (bv 32 0x0)) (! (== (var data_value) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var data_value)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er2,@er1" 01006992 0x0 (seq (storew 0 (cast 24 false (append (var e1) (var r1))) (append (var e2) (var r2))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e2) (var r2)) (bv 32 0x0)) (! (== (append (var e2) (var r2)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e2) (var r2))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er2,@(+4369,er1)" 01006f921111 0x0 (seq (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x1111))) (append (var e2) (var r2))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e2) (var r2)) (bv 32 0x0)) (! (== (append (var e2) (var r2)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e2) (var r2))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er2,@(+1118481,er1)" 010078906ba200111111 0x0 (seq (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111))) (append (var e2) (var r2))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e2) (var r2)) (bv 32 0x0)) (! (== (append (var e2) (var r2)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e2) (var r2))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er2,@-er1" 01006d92 0x0 (seq (set e1 (cast 16 false (>> (- (append (var e1) (var r1)) (bv 32 0x4)) (bv 8 0x10) false))) (set r1 (cast 16 false (- (append (var e1) (var r1)) (bv 32 0x4)))) (storew 0 (cast 24 false (append (var e1) (var r1))) (append (var e2) (var r2))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e2) (var r2)) (bv 32 0x0)) (! (== (append (var e2) (var r2)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e2) (var r2))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er1,@0x1111" 01006b811111 0x0 (seq (storew 0 (bv 24 0x1111) (append (var e1) (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e1) (var r1)) (bv 32 0x0)) (! (== (append (var e1) (var r1)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er1,@0xff8111" 01006b818111 0x0 (seq (storew 0 (bv 24 0xff8111) (append (var e1) (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e1) (var r1)) (bv 32 0x0)) (! (== (append (var e1) (var r1)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mov.l er1,@0x111111" 01006ba100111111 0x0 (seq (storew 0 (bv 24 0x111111) (append (var e1) (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e1) (var r1)) (bv 32 0x0)) (! (== (append (var e1) (var r1)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "movfpe @0x3344,r2l" 6a4a3344 0x0 (seq (set r2 (cast 16 false (| (& (cast 32 false (var r2)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (loadw 0 8 (bv 24 0x3344))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (loadw 0 8 (bv 24 0x3344)) (bv 8 0x0)) (! (== (loadw 0 8 (bv 24 0x3344)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (loadw 0 8 (bv 24 0x3344))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "movtpe r3l,@0x3322" 6acb3322 0x0 (seq (storew 0 (bv 24 0x3322) (cast 8 false (var r3))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (cast 8 false (var r3)) (bv 8 0x0)) (! (== (cast 8 false (var r3)) (bv 8 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (cast 8 false (var r3))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "mulxu.w r1,er2" 5212 0x0 (seq (set e2 (cast 16 false (>> (* (cast 32 false (var r1)) (& (append (var e2) (var r2)) (bv 32 0xffff))) (bv 8 0x10) false))) (set r2 (cast 16 false (* (cast 32 false (var r1)) (& (append (var e2) (var r2)) (bv 32 0xffff))))))
d "mulxs.b r1h,r2" 01c05012 0x0 (set r2 (* (cast 16 (msb (cast 8 false (>> (var r1) (bv 8 0x8) false))) (cast 8 false (>> (var r1) (bv 8 0x8) false))) (& (var r2) (bv 16 0xff))))
d "mulxs.w r1,er2" 01c05212 0x0 (seq (set e2 (cast 16 false (>> (* (cast 32 (msb (var r1)) (var r1)) (& (append (var e2) (var r2)) (bv 32 0xffff))) (bv 8 0x10) false))) (set r2 (cast 16 false (* (cast 32 (msb (var r1)) (var r1)) (& (append (var e2) (var r2)) (bv 32 0xffff))))))
d "not.w r1" 1711 0x0 (seq (set _res (~ (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set r1 (var _res)))
d "not.l er1" 1731 0x0 (seq (set _res (~ (append (var e1) (var r1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))))
d "neg.w r1" 1791 0x0 (seq (set _res (~- (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (& (bv 16 0x0) (bv 16 0xfff)) (+ (& (var r1) (bv 16 0xfff)) (ite false (bv 16 0x1) (bv 16 0x0)))) (bv 16 0x1000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 32 (msb (bv 16 0x0)) (bv 16 0x0)) (+ (cast 32 (msb (var r1)) (var r1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 32 (msb (bv 16 0x0)) (bv 16 0x0)) (+ (cast 32 (msb (var r1)) (var r1)) (ite false (bv 32 0x1) (bv 32 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (sle (- (cast 32 (msb (bv 16 0x0)) (bv 16 0x0)) (+ (cast 32 (msb (var r1)) (var r1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x0)) (! (== (- (cast 32 (msb (bv 16 0x0)) (bv 16 0x0)) (+ (cast 32 (msb (var r1)) (var r1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (bv 16 0x0)) (msb (var r1))) (^^ (msb (bv 16 0x0)) (! (is_zero (& (- (cast 32 (msb (bv 16 0x0)) (bv 16 0x0)) (+ (cast 32 (msb (var r1)) (var r1)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set r1 (var _res)))
d "neg.l er1" 17b1 0x0 (seq (set _res (~- (append (var e1) (var r1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (& (bv 32 0x0) (bv 32 0xfffffff)) (+ (& (append (var e1) (var r1)) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (sle (- (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)) (! (== (- (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (bv 32 0x0)) (msb (append (var e1) (var r1)))) (^^ (msb (bv 32 0x0)) (! (is_zero (& (- (cast 64 (msb (bv 32 0x0)) (bv 32 0x0)) (+ (cast 64 (msb (append (var e1) (var r1))) (append (var e1) (var r1))) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))))
d "or.w #0x1111,r1" 79411111 0x0 (seq (set _res (| (bv 16 0x1111) (var r1))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "or.w r1,r2" 6412 0x0 (seq (set _res (| (var r1) (var r2))) (set r2 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "or.l #0x11111111,er1" 7a4111111111 0x0 (seq (set _res (| (bv 32 0x11111111) (append (var e1) (var r1)))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "or.l er1,er2" 01f06412 0x0 (seq (set _res (| (append (var e1) (var r1)) (append (var e2) (var r2)))) (set e2 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r2 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "pop.l er1" 01006d71 0x0 (seq (set val (loadw 0 32 (cast 24 false (append (var e7) (var r7))))) (set e1 (cast 16 false (>> (var val) (bv 8 0x10) false))) (set r1 (cast 16 false (var val))) (set e7 (cast 16 false (>> (+ (append (var e7) (var r7)) (bv 32 0x4)) (bv 8 0x10) false))) (set r7 (cast 16 false (+ (append (var e7) (var r7)) (bv 32 0x4)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var val) (bv 32 0x0)) (! (== (var val) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var val)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "push.l er1" 01006df1 0x0 (seq (set e7 (cast 16 false (>> (- (append (var e7) (var r7)) (bv 32 0x4)) (bv 8 0x10) false))) (set r7 (cast 16 false (- (append (var e7) (var r7)) (bv 32 0x4)))) (storew 0 (cast 24 false (append (var e7) (var r7))) (append (var e1) (var r1))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (append (var e1) (var r1)) (bv 32 0x0)) (! (== (append (var e1) (var r1)) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "rotl.w r1" 1291 0x0 (seq (set result (<< (var r1) (bv 16 0x1) (msb (var r1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r1 (var result)))
d "rotr.w r1" 1391 0x0 (seq (set result (>> (var r1) (bv 16 0x1) (lsb (var r1)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r1 (var result)))
d "rotxl.w r1" 1211 0x0 (seq (set result (<< (var r1) (bv 16 0x1) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r1 (var result)))
d "rotxr.w r1" 1311 0x0 (seq (set result (>> (var r1) (bv 16 0x1) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (var r1)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r1 (var result)))
d "shal.w r0" 1090 0x0 (seq (set result (<< (var r0) (bv 16 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (^^ (msb (var result)) (msb (var r0))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (var r0)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r0 (var result)))
d "shll.w r0" 1010 0x0 (seq (set result (<< (var r0) (bv 16 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (var r0)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r0 (var result)))
d "shar.w r0" 1190 0x0 (seq (set result (>> (var r0) (bv 16 0x1) (msb (var r0)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (var r0)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r0 (var result)))
d "shlr.w r0" 1110 0x0 (seq (set result (>> (var r0) (bv 16 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 16 0x0)) (! (== (var result) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (var r0)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set r0 (var result)))
d "rotl.l er1" 12b1 0x0 (seq (set result (<< (append (var e1) (var r1)) (bv 32 0x1) (msb (append (var e1) (var r1))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e1 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r1 (cast 16 false (var result))))
d "rotr.l er1" 13b1 0x0 (seq (set result (>> (append (var e1) (var r1)) (bv 32 0x1) (lsb (append (var e1) (var r1))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e1 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r1 (cast 16 false (var result))))
d "rotxl.l er1" 1231 0x0 (seq (set result (<< (append (var e1) (var r1)) (bv 32 0x1) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e1 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r1 (cast 16 false (var result))))
d "rotxr.l er1" 1331 0x0 (seq (set result (>> (append (var e1) (var r1)) (bv 32 0x1) (! (is_zero (& (>> (cast 32 false (var ccr)) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (append (var e1) (var r1))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e1 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r1 (cast 16 false (var result))))
d "shal.l er0" 10b0 0x0 (seq (set result (<< (append (var e0) (var r0)) (bv 32 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (^^ (msb (var result)) (msb (append (var e0) (var r0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (append (var e0) (var r0))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e0 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r0 (cast 16 false (var result))))
d "shll.l er0" 1030 0x0 (seq (set result (<< (append (var e0) (var r0)) (bv 32 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (msb (append (var e0) (var r0))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e0 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r0 (cast 16 false (var result))))
d "shar.l er0" 11b0 0x0 (seq (set result (>> (append (var e0) (var r0)) (bv 32 0x1) (msb (append (var e0) (var r0))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (append (var e0) (var r0))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e0 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r0 (cast 16 false (var result))))
d "shlr.l er0" 1130 0x0 (seq (set result (>> (append (var e0) (var r0)) (bv 32 0x1) false)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var result) (bv 32 0x0)) (! (== (var result) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var result)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (lsb (append (var e0) (var r0))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set e0 (cast 16 false (>> (var result) (bv 8 0x10) false))) (set r0 (cast 16 false (var result))))
d "stc.w ccr,@er1" 01406990 0x0 (storew 0 (cast 24 false (append (var e1) (var r1))) (cast 16 false (var ccr)))
d "stc.w ccr,@(+4369,er1)" 01406f901111 0x0 (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x1111))) (cast 16 false (var ccr)))
d "stc.w ccr,@(+1118481,er1)" 014078106ba000111111 0x0 (storew 0 (cast 24 false (+ (append (var e1) (var r1)) (bv 32 0x111111))) (cast 16 false (var ccr)))
d "stc.w ccr,@-er1" 01406d90 0x0 (seq (set e1 (cast 16 false (>> (- (append (var e1) (var r1)) (bv 32 0x2)) (bv 8 0x10) false))) (set r1 (cast 16 false (- (append (var e1) (var r1)) (bv 32 0x2)))) (storew 0 (cast 24 false (append (var e1) (var r1))) (cast 16 false (var ccr))))
d "stc.w ccr,@0x1111" 01406b801111 0x0 (storew 0 (bv 24 0x1111) (cast 16 false (var ccr)))
d "stc.w ccr,@0x111111" 01406ba000111111 0x0 (storew 0 (bv 24 0x111111) (cast 16 false (var ccr)))
d "sub.w #0x1111,r1" 79311111 0x0 (seq (set _0 (bv 16 0x1111)) (set _1 (var r1)) (set r1 (- (var _1) (var _0))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (& (var _1) (bv 16 0xfff)) (+ (& (var _0) (bv 16 0xfff)) (ite false (bv 16 0x1) (bv 16 0x0)))) (bv 16 0x1000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 32 (msb (var _1)) (var _1)) (+ (cast 32 (msb (var _0)) (var _0)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 32 (msb (var _1)) (var _1)) (+ (cast 32 (msb (var _0)) (var _0)) (ite false (bv 32 0x1) (bv 32 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (sle (- (cast 32 (msb (var _1)) (var _1)) (+ (cast 32 (msb (var _0)) (var _0)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x0)) (! (== (- (cast 32 (msb (var _1)) (var _1)) (+ (cast 32 (msb (var _0)) (var _0)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (var _1)) (msb (var _0))) (^^ (msb (var _1)) (! (is_zero (& (- (cast 32 (msb (var _1)) (var _1)) (+ (cast 32 (msb (var _0)) (var _0)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x8000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "sub.l #0x11111111,er1" 7a3111111111 0x0 (seq (set _0 (bv 32 0x11111111)) (set _1 (append (var e1) (var r1))) (set e1 (cast 16 false (>> (- (var _1) (var _0)) (bv 8 0x10) false))) (set r1 (cast 16 false (- (var _1) (var _0)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (& (var _1) (bv 32 0xfffffff)) (+ (& (var _0) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (sle (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)) (! (== (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (var _1)) (msb (var _0))) (^^ (msb (var _1)) (! (is_zero (& (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "sub.l er1,er2" 1a92 0x0 (seq (set _0 (append (var e1) (var r1))) (set _1 (append (var e2) (var r2))) (set e2 (cast 16 false (>> (- (var _1) (var _0)) (bv 8 0x10) false))) (set r2 (cast 16 false (- (var _1) (var _0)))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (& (var _1) (bv 32 0xfffffff)) (+ (& (var _0) (bv 32 0xfffffff)) (ite false (bv 32 0x1) (bv 32 0x0)))) (bv 32 0x10000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x5) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x5) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (! (is_zero (& (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))) (& (<< (cast 32 false (ite (&& (sle (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)) (! (== (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x0) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x0) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite (&& (^^ (msb (var _1)) (msb (var _0))) (^^ (msb (var _1)) (! (is_zero (& (- (cast 64 (msb (var _1)) (var _1)) (+ (cast 64 (msb (var _0)) (var _0)) (ite false (bv 64 0x1) (bv 64 0x0)))) (bv 64 0x80000000)))))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "trapa #0x1" 5710 0x0 (seq (set e7 (cast 16 false (>> (- (append (var e7) (var r7)) (bv 32 0x4)) (bv 8 0x10) false))) (set r7 (cast 16 false (- (append (var e7) (var r7)) (bv 32 0x4)))) (storew 0 (cast 24 false (append (var e7) (var r7))) (bv 24 0x2)) (set e7 (cast 16 false (>> (- (append (var e7) (var r7)) (bv 32 0x2)) (bv 8 0x10) false))) (set r7 (cast 16 false (- (append (var e7) (var r7)) (bv 32 0x2)))) (storew 0 (cast 24 false (append (var e7) (var r7))) (var ccr)) (jmp (bv 24 0x24)))
d "xor.w #0x1111,r1" 79511111 0x0 (seq (set _res (^ (bv 16 0x1111) (var r1))) (set r1 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "xor.w r1,r2" 6512 0x0 (seq (set _res (^ (var r1) (var r2))) (set r2 (var _res)) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 16 0x0)) (! (== (var _res) (bv 16 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "xor.l #0x11111111,er1" 7a5111111111 0x0 (seq (set _res (^ (bv 32 0x11111111) (append (var e1) (var r1)))) (set e1 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r1 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
d "xor.l er1,er2" 01f06512 0x0 (seq (set _res (^ (append (var e1) (var r1)) (append (var e2) (var r2)))) (set e2 (cast 16 false (>> (var _res) (bv 8 0x10) false))) (set r2 (cast 16 false (var _res))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))) (& (<< (cast 32 false (ite (&& (sle (var _res) (bv 32 0x0)) (! (== (var _res) (bv 32 0x0)))) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x3) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x3) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))) (& (<< (cast 32 false (ite (is_zero (var _res)) (bv 16 0x1) (bv 16 0x0))) (bv 32 0x2) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x2) false))))) (set ccr (cast 8 false (| (& (cast 32 false (var ccr)) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))) (& (<< (cast 32 false (ite false (bv 16 0x1) (bv 16 0x0))) (bv 32 0x1) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false) (bv 32 0x1) false))))))
