d "bitrev d0" 00c0 0x0 (seq (set src (var d0)) (set res (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (| (bv 32 0x0) (<< (& (>> (var src) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1f) false)) (<< (& (>> (var src) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1e) false)) (<< (& (>> (var src) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1d) false)) (<< (& (>> (var src) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1c) false)) (<< (& (>> (var src) (bv 32 0x4) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1b) false)) (<< (& (>> (var src) (bv 32 0x5) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1a) false)) (<< (& (>> (var src) (bv 32 0x6) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x19) false)) (<< (& (>> (var src) (bv 32 0x7) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x18) false)) (<< (& (>> (var src) (bv 32 0x8) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x17) false)) (<< (& (>> (var src) (bv 32 0x9) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x16) false)) (<< (& (>> (var src) (bv 32 0xa) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x15) false)) (<< (& (>> (var src) (bv 32 0xb) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x14) false)) (<< (& (>> (var src) (bv 32 0xc) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x13) false)) (<< (& (>> (var src) (bv 32 0xd) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x12) false)) (<< (& (>> (var src) (bv 32 0xe) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x11) false)) (<< (& (>> (var src) (bv 32 0xf) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x10) false)) (<< (& (>> (var src) (bv 32 0x10) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xf) false)) (<< (& (>> (var src) (bv 32 0x11) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xe) false)) (<< (& (>> (var src) (bv 32 0x12) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xd) false)) (<< (& (>> (var src) (bv 32 0x13) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xc) false)) (<< (& (>> (var src) (bv 32 0x14) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xb) false)) (<< (& (>> (var src) (bv 32 0x15) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0xa) false)) (<< (& (>> (var src) (bv 32 0x16) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x9) false)) (<< (& (>> (var src) (bv 32 0x17) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x8) false)) (<< (& (>> (var src) (bv 32 0x18) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x7) false)) (<< (& (>> (var src) (bv 32 0x19) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x6) false)) (<< (& (>> (var src) (bv 32 0x1a) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x5) false)) (<< (& (>> (var src) (bv 32 0x1b) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x4) false)) (<< (& (>> (var src) (bv 32 0x1c) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x3) false)) (<< (& (>> (var src) (bv 32 0x1d) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x2) false)) (<< (& (>> (var src) (bv 32 0x1e) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)) (bv 8 0x1) false)) (& (>> (var src) (bv 32 0x1f) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (set d0 (cast 32 false (var res))))
d "byterev d1" 02c1 0x0 (seq (set src (var d1)) (set res (| (| (<< (& (var src) (bv 32 0xff)) (bv 8 0x18) false) (<< (& (var src) (bv 32 0xff00)) (bv 8 0x8) false)) (| (& (>> (var src) (bv 8 0x8) false) (bv 32 0xff00)) (>> (var src) (bv 8 0x18) false)))) (set d1 (cast 32 false (var res))))
d "ff1 d2" 04c2 0x0 (seq (set src (var d2)) (set res (ite (! (is_zero (& (>> (var src) (bv 32 0x1f) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x0) (ite (! (is_zero (& (>> (var src) (bv 32 0x1e) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1) (ite (! (is_zero (& (>> (var src) (bv 32 0x1d) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x2) (ite (! (is_zero (& (>> (var src) (bv 32 0x1c) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x3) (ite (! (is_zero (& (>> (var src) (bv 32 0x1b) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x4) (ite (! (is_zero (& (>> (var src) (bv 32 0x1a) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x5) (ite (! (is_zero (& (>> (var src) (bv 32 0x19) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x6) (ite (! (is_zero (& (>> (var src) (bv 32 0x18) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x7) (ite (! (is_zero (& (>> (var src) (bv 32 0x17) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x8) (ite (! (is_zero (& (>> (var src) (bv 32 0x16) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x9) (ite (! (is_zero (& (>> (var src) (bv 32 0x15) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xa) (ite (! (is_zero (& (>> (var src) (bv 32 0x14) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xb) (ite (! (is_zero (& (>> (var src) (bv 32 0x13) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xc) (ite (! (is_zero (& (>> (var src) (bv 32 0x12) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xd) (ite (! (is_zero (& (>> (var src) (bv 32 0x11) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xe) (ite (! (is_zero (& (>> (var src) (bv 32 0x10) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0xf) (ite (! (is_zero (& (>> (var src) (bv 32 0xf) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x10) (ite (! (is_zero (& (>> (var src) (bv 32 0xe) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x11) (ite (! (is_zero (& (>> (var src) (bv 32 0xd) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x12) (ite (! (is_zero (& (>> (var src) (bv 32 0xc) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x13) (ite (! (is_zero (& (>> (var src) (bv 32 0xb) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x14) (ite (! (is_zero (& (>> (var src) (bv 32 0xa) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x15) (ite (! (is_zero (& (>> (var src) (bv 32 0x9) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x16) (ite (! (is_zero (& (>> (var src) (bv 32 0x8) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x17) (ite (! (is_zero (& (>> (var src) (bv 32 0x7) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x18) (ite (! (is_zero (& (>> (var src) (bv 32 0x6) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x19) (ite (! (is_zero (& (>> (var src) (bv 32 0x5) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1a) (ite (! (is_zero (& (>> (var src) (bv 32 0x4) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1b) (ite (! (is_zero (& (>> (var src) (bv 32 0x3) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1c) (ite (! (is_zero (& (>> (var src) (bv 32 0x2) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1d) (ite (! (is_zero (& (>> (var src) (bv 32 0x1) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1e) (ite (! (is_zero (& (>> (var src) (bv 32 0x0) false) (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x1)) false)))) (bv 32 0x1f) (bv 32 0x20)))))))))))))))))))))))))))))))))) (set d2 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (var src)) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (var src)) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "strldsr.w 0x4d2" 40e746fc04d2 0x0 (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege))
d "strldsr.w 0x24d2" 40e746fc24d2 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set push_value (cast 32 false (var sr))) (set a7 (cast 32 false (- (var a7) (bv 32 0x4)))) (storew 0 (var a7) (cast 32 false (var push_value))) (set sr_write_value (cast 16 false (bv 16 0x24d2))) (branch (! (== (ite (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)) (ite (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)))) (seq (branch (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set isp (cast 32 false (var a7))) (set usp (cast 32 false (var a7)))) (branch (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set a7 (cast 32 false (var isp))) (set a7 (cast 32 false (var usp))))) empty) (set sr (var sr_write_value))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "move.w ccr, d3" 42c3 0x0 (seq (set src (cast 16 false (cast 8 false (var sr)))) (set d3 (| (& (var d3) (bv 32 0xffff0000)) (cast 32 false (var src)))))
d "move.w d0, sr" 46c0 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (set sr_write_value (cast 16 false (var src))) (branch (! (== (ite (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)) (ite (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)))) (seq (branch (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set isp (cast 32 false (var a7))) (set usp (cast 32 false (var a7)))) (branch (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set a7 (cast 32 false (var isp))) (set a7 (cast 32 false (var usp))))) empty) (set sr (var sr_write_value))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "movem.l d0-d1, (a0)" 48d00003 0x0 (seq (set addr (cast 32 false (var a0))) (storew 0 (var addr) (cast 32 false (var d0))) (storew 0 (+ (var addr) (bv 32 0x4)) (cast 32 false (var d1))))
d "sats.l d0" 4c80 0x0 (seq (set src (var d0)) (set res (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (ite (msb (var src)) (bv 32 0x7fffffff) (bv 32 0x80000000)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "link.w a0, 0x4" 4e500004 0x0 (seq (set push_value (var a0)) (set a7 (cast 32 false (- (var a7) (bv 32 0x4)))) (storew 0 (var a7) (cast 32 false (var push_value))) (set a0 (cast 32 false (var a7))) (set new_sp (+ (var a7) (bv 32 0x4))) (set a7 (cast 32 false (var new_sp))))
d "move usp, a0" 4e68 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var usp)) (set a0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "stop 0x2700" 4e722700 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set system_op (bv 32 0x1)) (set system_sr (bv 32 0x2700)) (set sr_write_value (cast 16 false (bv 16 0x2700))) (branch (! (== (ite (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)) (ite (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (bv 8 0x1) (bv 8 0x0)))) (seq (branch (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set isp (cast 32 false (var a7))) (set usp (cast 32 false (var a7)))) (branch (&& (! (is_zero (& (cast 16 false (var sr_write_value)) (bv 16 0x2000)))) (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10))))) (set a7 (cast 32 false (var isp))) (set a7 (cast 32 false (var usp))))) empty) (set sr (var sr_write_value)) (goto m68k_system)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "movec cacr, d1" 4e7a1002 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (set d1 (cast 32 false (var cacr))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "movec d0, cacr" 4e7b0002 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set cacr_write_value (cast 32 false (var d0))) (branch (&& (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (^^ (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10)))) (! (is_zero (& (cast 32 false (var cacr_write_value)) (bv 32 0x10)))))) (branch (! (is_zero (& (cast 32 false (var cacr)) (bv 32 0x10)))) (seq (set isp (cast 32 false (var a7))) (set a7 (cast 32 false (var usp)))) (seq (set usp (cast 32 false (var a7))) (set a7 (cast 32 false (var isp))))) empty) (set cacr (var cacr_write_value))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "tpf.w 0x1234" 51fa1234 0x0 nop
d "tpf.l 0x12345678" 51fb12345678 0x0 nop
d "tpf" 51fc 0x0 nop
d "addq.l 0x1, d0" 5280 0x0 (seq (set src (bv 32 0x1)) (set dst (var d0)) (set res (+ (var dst) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (& (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite (&& (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (msb (var src)) (bv 1 0x1) (bv 1 0x0))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (msb (var res)) (bv 1 0x1) (bv 1 0x0))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite (&& (ule (var res) (var dst)) (! (== (var res) (var dst)))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (&& (ule (var res) (var dst)) (! (== (var res) (var dst)))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
d "subq.l 0x1, d0" 5380 0x0 (seq (set src (bv 32 0x1)) (set dst (var d0)) (set res (- (var dst) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (& (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite (&& (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (msb (var src)) (bv 1 0x1) (bv 1 0x0)))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (msb (var res)) (bv 1 0x1) (bv 1 0x0))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite (&& (ule (var dst) (var src)) (! (== (var dst) (var src)))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (&& (ule (var dst) (var src)) (! (== (var dst) (var src)))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
d "bra.l 0x12" 60ff00000010 0x0 (jmp (bv 32 0x12))
d "bsr.l 0x12" 61ff00000010 0x0 (seq (set push_value (bv 32 0x6)) (set a7 (cast 32 false (- (var a7) (bv 32 0x4)))) (storew 0 (var a7) (cast 32 false (var push_value))) (jmp (bv 32 0x12)))
d "bne.l 0x12" 66ff00000010 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) (jmp (bv 32 0x12)) empty)
d "mvs.b d0, d0" 7100 0x0 (seq (set src (cast 8 false (var d0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b (a0)+, d0" 7118 0x0 (seq (set src (loadw 0 8 (var a0))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b -(a0), d0" 7120 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set src (loadw 0 8 (var a0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x0(a0), d0" 71280000 0x0 (seq (set src (loadw 0 8 (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x0(a0, d0.w), d0" 71300000 0x0 (seq (set src (loadw 0 8 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b (a0, d0.w), d0" 71300100 0x0 (seq (set src (loadw 0 8 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b ([0x18001ff, a0], 0x8000fff), d0" 7130017f018001ff08000fff 0x0 (seq (set src (loadw 0 8 (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x0.w, d0" 71380000 0x0 (seq (set src (loadw 0 8 (bv 32 0x0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x1.l, d0" 713900000001 0x0 (seq (set src (loadw 0 8 (bv 32 0x1))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x2(pc), d0" 713a0000 0x0 (seq (set src (loadw 0 8 (bv 32 0x2))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x2(pc, d0.w), d0" 713b0000 0x0 (seq (set src (loadw 0 8 (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b ([0x1800201, pc], 0x8000fff), d0" 713b017f018001ff08000fff 0x0 (seq (set src (loadw 0 8 (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b 0x0, d0" 713c0000 0x0 (seq (set src (bv 8 0x0)) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w d0, d0" 7140 0x0 (seq (set src (cast 16 false (var d0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w a0, d0" 7148 0x0 (seq (set src (cast 16 false (var a0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w (a0), d0" 7150 0x0 (seq (set src (loadw 0 16 (var a0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w (a0)+, d0" 7158 0x0 (seq (set src (loadw 0 16 (var a0))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w -(a0), d0" 7160 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set src (loadw 0 16 (var a0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x0(a0), d0" 71680000 0x0 (seq (set src (loadw 0 16 (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x0(a0, d0.w), d0" 71700000 0x0 (seq (set src (loadw 0 16 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w (a0, d0.w), d0" 71700100 0x0 (seq (set src (loadw 0 16 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w ([0x18001ff, a0], 0x8000fff), d0" 7170017f018001ff08000fff 0x0 (seq (set src (loadw 0 16 (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x0.w, d0" 71780000 0x0 (seq (set src (loadw 0 16 (bv 32 0x0))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x1.l, d0" 717900000001 0x0 (seq (set src (loadw 0 16 (bv 32 0x1))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x2(pc), d0" 717a0000 0x0 (seq (set src (loadw 0 16 (bv 32 0x2))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x2(pc, d0.w), d0" 717b0000 0x0 (seq (set src (loadw 0 16 (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w ([0x1800201, pc], 0x8000fff), d0" 717b017f018001ff08000fff 0x0 (seq (set src (loadw 0 16 (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.w 0x0, d0" 717c0000 0x0 (seq (set src (bv 16 0x0)) (set res (cast 32 (msb (var src)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b d0, d0" 7180 0x0 (seq (set src (cast 8 false (var d0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b (a0), d0" 7190 0x0 (seq (set src (loadw 0 8 (var a0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b (a0)+, d0" 7198 0x0 (seq (set src (loadw 0 8 (var a0))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b -(a0), d0" 71a0 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set src (loadw 0 8 (var a0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x0(a0), d0" 71a80000 0x0 (seq (set src (loadw 0 8 (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x0(a0, d0.w), d0" 71b00000 0x0 (seq (set src (loadw 0 8 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b (a0, d0.w), d0" 71b00100 0x0 (seq (set src (loadw 0 8 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b ([0x18001ff, a0], 0x8000fff), d0" 71b0017f018001ff08000fff 0x0 (seq (set src (loadw 0 8 (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x0.w, d0" 71b80000 0x0 (seq (set src (loadw 0 8 (bv 32 0x0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x1.l, d0" 71b900000001 0x0 (seq (set src (loadw 0 8 (bv 32 0x1))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x2(pc), d0" 71ba0000 0x0 (seq (set src (loadw 0 8 (bv 32 0x2))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x2(pc, d0.w), d0" 71bb0000 0x0 (seq (set src (loadw 0 8 (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b ([0x1800201, pc], 0x8000fff), d0" 71bb017f018001ff08000fff 0x0 (seq (set src (loadw 0 8 (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.b 0x0, d0" 71bc0000 0x0 (seq (set src (bv 8 0x0)) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w d0, d0" 71c0 0x0 (seq (set src (cast 16 false (var d0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w a0, d0" 71c8 0x0 (seq (set src (cast 16 false (var a0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w (a0)+, d0" 71d8 0x0 (seq (set src (loadw 0 16 (var a0))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w -(a0), d0" 71e0 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set src (loadw 0 16 (var a0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x0(a0), d0" 71e80000 0x0 (seq (set src (loadw 0 16 (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x0(a0, d0.w), d0" 71f00000 0x0 (seq (set src (loadw 0 16 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w (a0, d0.w), d0" 71f00100 0x0 (seq (set src (loadw 0 16 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w ([0x18001ff, a0], 0x8000fff), d0" 71f0017f018001ff08000fff 0x0 (seq (set src (loadw 0 16 (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x0.w, d0" 71f80000 0x0 (seq (set src (loadw 0 16 (bv 32 0x0))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x1.l, d0" 71f900000001 0x0 (seq (set src (loadw 0 16 (bv 32 0x1))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x2(pc), d0" 71fa0000 0x0 (seq (set src (loadw 0 16 (bv 32 0x2))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x2(pc, d0.w), d0" 71fb0000 0x0 (seq (set src (loadw 0 16 (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w ([0x1800201, pc], 0x8000fff), d0" 71fb017f018001ff08000fff 0x0 (seq (set src (loadw 0 16 (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w 0x0, d0" 71fc0000 0x0 (seq (set src (bv 16 0x0)) (set res (cast 32 false (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b d0, d1" 7300 0x0 (seq (set src (cast 8 false (var d0))) (set res (cast 32 (msb (var src)) (var src))) (set d1 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvs.b (a0), d1" 7310 0x0 (seq (set src (loadw 0 8 (var a0))) (set res (cast 32 (msb (var src)) (var src))) (set d1 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mvz.w (a0), d1" 73d0 0x0 (seq (set src (loadw 0 16 (var a0))) (set res (cast 32 false (var src))) (set d1 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, d0" a140 0x0 (seq (set res (bv 32 0xffffffff)) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, a0" a148 0x0 (seq (set res (bv 32 0xffffffff)) (set a0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, (a0)+" a158 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (var a0) (cast 32 false (var res))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, -(a0)" a160 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set res (bv 32 0xffffffff)) (storew 0 (var a0) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x0(a0)" a1680000 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x0(a0, d0.w)" a1700000 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, (a0, d0.w)" a1700100 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, ([0x18001ff, a0], 0x8000fff)" a170017f018001ff08000fff 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x0.w" a1780000 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (bv 32 0x0) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x1.l" a17900000001 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (bv 32 0x1) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x2(pc)" a17a0000 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (bv 32 0x2) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x2(pc, d0.w)" a17b0000 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, ([0x1800201, pc], 0x8000fff)" a17b017f018001ff08000fff 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0xffffffff, 0x1" a17c00000001 0x0 (seq (set res (bv 32 0xffffffff)) (storew 0 (bv 32 0x1) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "mov3q.l 0x2, (a4)" a554 0x0 (seq (set res (bv 32 0x2)) (storew 0 (var a4) (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "intouch (a0)" f428 0x0 (seq (set cache_addr (cast 32 false (var a0))) (set cache_op (bv 32 0x0)) (goto m68k_cache))
d "cpushl bc, (a0)" f4e8 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set cache_addr (cast 32 false (var a0))) (set cache_op (bv 32 0x2)) (set cache_selector (bv 32 0x3)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "wddata.b (a0)" fb10 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b (a0)+" fb18 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 8 (var debug_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b -(a0)" fb20 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b 0x0(a0)" fb280000 0x0 (seq (set debug_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b 0x0(a0, d0.w)" fb300000 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b (a0, d0.w)" fb300100 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b ([0x18001ff, a0], 0x8000fff)" fb30017f018001ff08000fff 0x0 (seq (set debug_addr (cast 32 false (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b 0x0.w" fb380000 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x0))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.b 0x1.l" fb3900000001 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x1))) (set debug_data (loadw 0 8 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x8)) (goto m68k_debug))
d "wddata.w (a0)" fb50 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w (a0)+" fb58 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 16 (var debug_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w -(a0)" fb60 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w 0x0(a0)" fb680000 0x0 (seq (set debug_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w 0x0(a0, d0.w)" fb700000 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w (a0, d0.w)" fb700100 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w ([0x18001ff, a0], 0x8000fff)" fb70017f018001ff08000fff 0x0 (seq (set debug_addr (cast 32 false (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w 0x0.w" fb780000 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x0))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.w 0x1.l" fb7900000001 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x1))) (set debug_data (loadw 0 16 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x10)) (goto m68k_debug))
d "wddata.l (a0)" fb90 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l (a0)+" fb98 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 32 (var debug_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l -(a0)" fba0 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l 0x0(a0)" fba80000 0x0 (seq (set debug_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l 0x0(a0, d0.w)" fbb00000 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l (a0, d0.w)" fbb00100 0x0 (seq (set debug_addr (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l ([0x18001ff, a0], 0x8000fff)" fbb0017f018001ff08000fff 0x0 (seq (set debug_addr (cast 32 false (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l 0x0.w" fbb80000 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x0))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wddata.l 0x1.l" fbb900000001 0x0 (seq (set debug_addr (cast 32 false (bv 32 0x1))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x0)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "wdebug.l (a0)" fbd00003 0x0 (seq (set debug_addr (cast 32 false (var a0))) (set debug_data (loadw 0 32 (var debug_addr))) (set debug_op (bv 32 0x1)) (set debug_bits (bv 32 0x20)) (goto m68k_debug))
d "cp0ld.b d0, d0, 0x1, 0x1" fc000001 0x0 (seq (set cp_data (cast 8 false (var d0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0nop 0x8" fc000e00 0x0 (seq (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x0)) (set cp_extension (bv 32 0x8)) (goto m68k_coprocessor))
d "cp0ld.b d0, a0, 0x1, 0x0" fc008000 0x0 (seq (set cp_data (cast 8 false (var d0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b a0, d0, 0x1, 0x0" fc080000 0x0 (seq (set cp_data (cast 8 false (var a0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b a0, a0, 0x1, 0x0" fc088000 0x0 (seq (set cp_data (cast 8 false (var a0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b (a0), d0, 0x1, 0x0" fc100000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b (a0), a0, 0x1, 0x0" fc108000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b (a0)+, d0, 0x1, 0x0" fc180000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b (a0)+, a2, 0x6, 0x1" fc18aa01 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x6)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0ld.b -(a0), d0, 0x1, 0x0" fc200000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b -(a0), a0, 0x1, 0x0" fc208000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b 0x1(a0), d0, 0x1, 0x0" fc2800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.b -0x7f00(a0), a0, 0x1, 0x0" fc2880008100 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w d0, d0, 0x1, 0x1" fc400001 0x0 (seq (set cp_data (cast 16 false (var d0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0ld.w d0, a0, 0x1, 0x0" fc408000 0x0 (seq (set cp_data (cast 16 false (var d0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w a0, d0, 0x1, 0x0" fc480000 0x0 (seq (set cp_data (cast 16 false (var a0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w a0, a0, 0x1, 0x0" fc488000 0x0 (seq (set cp_data (cast 16 false (var a0))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w (a0), d0, 0x1, 0x0" fc500000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w (a0), a2, 0x3, 0x1" fc50a401 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x3)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0ld.w (a0)+, d0, 0x1, 0x0" fc580000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w (a0)+, a0, 0x1, 0x0" fc588000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w -(a0), d0, 0x1, 0x0" fc600000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w -(a0), a0, 0x1, 0x0" fc608000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w 0x1(a0), d0, 0x1, 0x0" fc6800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.w -0x7f00(a0), a0, 0x1, 0x0" fc6880008100 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0nop 0x3" fc800400 0x0 (seq (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x0)) (set cp_extension (bv 32 0x3)) (goto m68k_coprocessor))
d "cp0ld.l d0, d1, 0x3, 0x0" fc801400 0x0 (seq (set cp_data (var d0)) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x3)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l d0, d2, 0x1, 0x123" fc802123 0x0 (seq (set cp_data (var d0)) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x123)) (goto m68k_coprocessor))
d "cp0ld.l d0, a0, 0x1, 0x0" fc808000 0x0 (seq (set cp_data (var d0)) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l a0, d0, 0x1, 0x0" fc880000 0x0 (seq (set cp_data (var a0)) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l a0, a0, 0x1, 0x0" fc888000 0x0 (seq (set cp_data (var a0)) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l (a0), d0, 0x1, 0x0" fc900000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l (a0), a0, 0x1, 0x0" fc908000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l (a0)+, d0, 0x1, 0x0" fc980000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l (a0)+, a0, 0x1, 0x0" fc988000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l -(a0), d0, 0x1, 0x0" fca00000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l -(a0), a0, 0x1, 0x0" fca08000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l 0x1(a0), d0, 0x1, 0x0" fca800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0ld.l 0x10(a0), a2, 0x8, 0x1" fca8ae010010 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x10))))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x8)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0bcbusy 0x52" fcc00050 0x0 (seq (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x1)) (set cp_branch (bv 32 0x52)) (goto m68k_coprocessor))
d "cp0st.b d0, d0, 0x1, 0x0" fd000000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, d0, 0x1, 0x0" fd008000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b d0, a0, 0x1, 0x0" fd080000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, a0, 0x1, 0x0" fd088000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b d0, (a0), 0x1, 0x0" fd100000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, (a0), 0x1, 0x0" fd108000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b d0, (a0)+, 0x1, 0x0" fd180000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, (a0)+, 0x1, 0x0" fd188000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b d0, -(a0), 0x1, 0x0" fd200000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, -(a0), 0x1, 0x0" fd208000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b d0, 0x1(a0), 0x1, 0x0" fd2800000001 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.b a0, -0x7f00(a0), 0x1, 0x0" fd2880008100 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w d0, d0, 0x1, 0x0" fd400000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a0, d0, 0x1, 0x0" fd408000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w d0, a0, 0x1, 0x0" fd480000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 (msb (var cp_data)) (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a0, a0, 0x1, 0x0" fd488000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 (msb (var cp_data)) (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w d0, (a0), 0x1, 0x0" fd500000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a2, (a0), 0x3, 0x1" fd50a401 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x3)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp0st.w d0, (a0)+, 0x1, 0x0" fd580000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a0, (a0)+, 0x1, 0x0" fd588000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w d0, -(a0), 0x1, 0x0" fd600000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a0, -(a0), 0x1, 0x0" fd608000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w d0, 0x1(a0), 0x1, 0x0" fd6800000001 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.w a0, -0x7f00(a0), 0x1, 0x0" fd6880008100 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d2, d0, 0x1, 0x123" fd802123 0x0 (seq (set cp_data (var cp_external_data)) (set d0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x123)) (goto m68k_coprocessor))
d "cp0st.l a0, d0, 0x1, 0x0" fd808000 0x0 (seq (set cp_data (var cp_external_data)) (set d0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d0, a0, 0x1, 0x0" fd880000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l a0, a0, 0x1, 0x0" fd888000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d0, (a0), 0x1, 0x0" fd900000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l a0, (a0), 0x1, 0x0" fd908000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d0, (a0)+, 0x1, 0x0" fd980000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l a0, (a0)+, 0x1, 0x0" fd988000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d0, -(a0), 0x1, 0x0" fda00000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l a0, -(a0), 0x1, 0x0" fda08000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l d0, 0x1(a0), 0x1, 0x0" fda800000001 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp0st.l a0, -0x7f00(a0), 0x1, 0x0" fda880008100 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x0)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b d0, d0, 0x1, 0x1" fe000001 0x0 (seq (set cp_data (cast 8 false (var d0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp1nop 0x8" fe000e00 0x0 (seq (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x0)) (set cp_extension (bv 32 0x8)) (goto m68k_coprocessor))
d "cp1ld.b d0, a0, 0x1, 0x0" fe008000 0x0 (seq (set cp_data (cast 8 false (var d0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b a0, d0, 0x1, 0x0" fe080000 0x0 (seq (set cp_data (cast 8 false (var a0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b a0, a0, 0x1, 0x0" fe088000 0x0 (seq (set cp_data (cast 8 false (var a0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b (a0), d0, 0x1, 0x0" fe100000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b (a0), a0, 0x1, 0x0" fe108000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b (a0)+, d0, 0x1, 0x0" fe180000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b (a0)+, a0, 0x1, 0x0" fe188000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b -(a0), d0, 0x1, 0x0" fe200000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b -(a0), a0, 0x1, 0x0" fe208000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b 0x1(a0), d0, 0x1, 0x0" fe2800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.b -0x7f00(a0), a0, 0x1, 0x0" fe2880008100 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (set cp_data (loadw 0 8 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w d0, d0, 0x1, 0x1" fe400001 0x0 (seq (set cp_data (cast 16 false (var d0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x1)) (goto m68k_coprocessor))
d "cp1ld.w d0, a0, 0x1, 0x0" fe408000 0x0 (seq (set cp_data (cast 16 false (var d0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w a0, d0, 0x1, 0x0" fe480000 0x0 (seq (set cp_data (cast 16 false (var a0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w a0, a0, 0x1, 0x0" fe488000 0x0 (seq (set cp_data (cast 16 false (var a0))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w (a0), d0, 0x1, 0x0" fe500000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w (a0), a0, 0x1, 0x0" fe508000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w (a0)+, d0, 0x1, 0x0" fe580000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w (a0)+, a0, 0x1, 0x0" fe588000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w -(a0), d0, 0x1, 0x0" fe600000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w -(a0), a0, 0x1, 0x0" fe608000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w 0x1(a0), d0, 0x1, 0x0" fe6800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.w -0x7f00(a0), a0, 0x1, 0x0" fe6880008100 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (set cp_data (loadw 0 16 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l d0, d2, 0x1, 0x123" fe802123 0x0 (seq (set cp_data (var d0)) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x123)) (goto m68k_coprocessor))
d "cp1ld.l d0, a0, 0x1, 0x0" fe808000 0x0 (seq (set cp_data (var d0)) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l a0, d0, 0x1, 0x0" fe880000 0x0 (seq (set cp_data (var a0)) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l a0, a0, 0x1, 0x0" fe888000 0x0 (seq (set cp_data (var a0)) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l (a0), d0, 0x1, 0x0" fe900000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l (a0), a0, 0x1, 0x0" fe908000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l (a0)+, d0, 0x1, 0x0" fe980000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l (a0)+, a0, 0x1, 0x0" fe988000 0x0 (seq (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l -(a0), d0, 0x1, 0x0" fea00000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l -(a0), a0, 0x1, 0x0" fea08000 0x0 (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l 0x1(a0), d0, 0x1, 0x0" fea800000001 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1ld.l -0x7f00(a0), a0, 0x1, 0x0" fea880008100 0x0 (seq (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (set cp_data (loadw 0 32 (var cp_addr))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x2)) (set cp_store (bv 32 0x0)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1bcbusy 0x52" fec00050 0x0 (seq (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x1)) (set cp_branch (bv 32 0x52)) (goto m68k_coprocessor))
d "cp1st.b d0, d0, 0x1, 0x0" ff000000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, d0, 0x1, 0x0" ff008000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b d0, a0, 0x1, 0x0" ff080000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, a0, 0x1, 0x0" ff088000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b d0, (a0), 0x1, 0x0" ff100000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, (a0), 0x1, 0x0" ff108000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b d0, (a0)+, 0x1, 0x0" ff180000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, (a0)+, 0x1, 0x0" ff188000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b d0, -(a0), 0x1, 0x0" ff200000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, -(a0), 0x1, 0x0" ff208000 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b d0, 0x1(a0), 0x1, 0x0" ff2800000001 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.b a0, -0x7f00(a0), 0x1, 0x0" ff2880008100 0x0 (seq (set cp_data (cast 8 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 8 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x8)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, d0, 0x1, 0x0" ff400000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, d0, 0x1, 0x0" ff408000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var cp_data)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, a0, 0x1, 0x0" ff480000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 (msb (var cp_data)) (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, a0, 0x1, 0x0" ff488000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 (msb (var cp_data)) (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, (a0), 0x1, 0x0" ff500000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, (a0), 0x1, 0x0" ff508000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, (a0)+, 0x1, 0x0" ff580000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, (a0)+, 0x1, 0x0" ff588000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, -(a0), 0x1, 0x0" ff600000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, -(a0), 0x1, 0x0" ff608000 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w d0, 0x1(a0), 0x1, 0x0" ff6800000001 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.w a0, -0x7f00(a0), 0x1, 0x0" ff6880008100 0x0 (seq (set cp_data (cast 16 false (var cp_external_data))) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 16 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x10)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d2, d0, 0x1, 0x123" ff802123 0x0 (seq (set cp_data (var cp_external_data)) (set d0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x123)) (goto m68k_coprocessor))
d "cp1st.l a0, d0, 0x1, 0x0" ff808000 0x0 (seq (set cp_data (var cp_external_data)) (set d0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d0, a0, 0x1, 0x0" ff880000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l a0, a0, 0x1, 0x0" ff888000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d0, (a0), 0x1, 0x0" ff900000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l a0, (a0), 0x1, 0x0" ff908000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d0, (a0)+, 0x1, 0x0" ff980000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l a0, (a0)+, 0x1, 0x0" ff988000 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d0, -(a0), 0x1, 0x0" ffa00000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l a0, -(a0), 0x1, 0x0" ffa08000 0x0 (seq (set cp_data (var cp_external_data)) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set cp_addr (cast 32 false (var a0))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l d0, 0x1(a0), 0x1, 0x0" ffa800000001 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
d "cp1st.l a0, -0x7f00(a0), 0x1, 0x0" ffa880008100 0x0 (seq (set cp_data (var cp_external_data)) (set cp_addr (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xffff8100))))) (storew 0 (var cp_addr) (cast 32 false (var cp_data))) (set cp_num (bv 32 0x1)) (set cp_op (bv 32 0x3)) (set cp_store (bv 32 0x1)) (set cp_bits (bv 32 0x20)) (set cp_selector (bv 32 0x1)) (set cp_extension (bv 32 0x0)) (goto m68k_coprocessor))
