d "add fp0" f200007f
d "add fp0, fp1" f20000ff
d "fsmove fp1, fp2" f2000540
d "fssqrt fp1, fp2" f2000541
d "fdmove fp1, fp2" f2000544
d "fdsqrt fp1, fp2" f2000545
d "fsabs fp1, fp2" f2000558
d "fsneg fp1, fp2" f200055a
d "fdabs fp1, fp2" f200055c
d "fdneg fp1, fp2" f200055e
d "fsdiv fp1, fp2" f2000560
d "fsadd fp1, fp2" f2000562
d "fsmul fp1, fp2" f2000563
d "fddiv fp1, fp2" f2000564
d "fdadd fp1, fp2" f2000566
d "fdmul fp1, fp2" f2000567
d "fssub fp1, fp2" f2000568
d "fdsub fp1, fp2" f200056c
d "cinvl nc, (a0)" f408 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 0x1)) (set cache_selector (bv 32 0x0)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "cinvp nc, (a0)" f410 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 0x1)) (set cache_selector (bv 32 0x0)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "cinva nc" f418 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set cache_op (bv 32 0x1)) (set cache_selector (bv 32 0x0)) (set cache_all (bv 32 0x1)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "cpushp nc, (a0)" f430 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 0x0)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "cpusha nc" f438 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set cache_op (bv 32 0x2)) (set cache_selector (bv 32 0x0)) (set cache_all (bv 32 0x1)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "cpushl dc, (a0)" f468 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 0x1)) (goto m68k_cache)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "pflushn (a0)" f500 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_addr (cast 32 false (var a0))) (set mmu_op (bv 32 0x1)) (set mmu_flush_non_global (bv 32 0x1)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "pflush (a0)" f508 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_addr (cast 32 false (var a0))) (set mmu_op (bv 32 0x1)) (set mmu_flush_non_global (bv 32 0x0)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "pflushan" f510 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_op (bv 32 0x1)) (set mmu_flush_non_global (bv 32 0x1)) (set mmu_flush_all (bv 32 0x1)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "pflusha" f518 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_op (bv 32 0x1)) (set mmu_flush_non_global (bv 32 0x0)) (set mmu_flush_all (bv 32 0x1)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "ptestw (a0)" f548 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_addr (cast 32 false (var a0))) (set mmu_op (bv 32 0x2)) (set mmu_rw (bv 32 0x1)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "ptestr (a0)" f568 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set mmu_addr (cast 32 false (var a0))) (set mmu_op (bv 32 0x2)) (set mmu_rw (bv 32 0x0)) (goto m68k_mmu)) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "move16 (a0)+, 0x1.l" f60000000001 0x0 (seq (set src_addr (var a0)) (set dst_addr (cast 32 false (bv 32 0x1))) (set src_line (& (var src_addr) (bv 32 0xfffffff0))) (set dst_line (& (var dst_addr) (bv 32 0xfffffff0))) (set word0 (loadw 0 32 (var src_line))) (set word1 (loadw 0 32 (+ (var src_line) (bv 32 0x4)))) (set word2 (loadw 0 32 (+ (var src_line) (bv 32 0x8)))) (set word3 (loadw 0 32 (+ (var src_line) (bv 32 0xc)))) (storew 0 (var dst_line) (cast 32 false (var word0))) (storew 0 (+ (var dst_line) (bv 32 0x4)) (cast 32 false (var word1))) (storew 0 (+ (var dst_line) (bv 32 0x8)) (cast 32 false (var word2))) (storew 0 (+ (var dst_line) (bv 32 0xc)) (cast 32 false (var word3))) (set a0 (cast 32 false (+ (var src_addr) (bv 32 0x10)))))
d "move16 0x1.l, (a0)+" f60800000001 0x0 (seq (set src_addr (cast 32 false (bv 32 0x1))) (set dst_addr (var a0)) (set src_line (& (var src_addr) (bv 32 0xfffffff0))) (set dst_line (& (var dst_addr) (bv 32 0xfffffff0))) (set word0 (loadw 0 32 (var src_line))) (set word1 (loadw 0 32 (+ (var src_line) (bv 32 0x4)))) (set word2 (loadw 0 32 (+ (var src_line) (bv 32 0x8)))) (set word3 (loadw 0 32 (+ (var src_line) (bv 32 0xc)))) (storew 0 (var dst_line) (cast 32 false (var word0))) (storew 0 (+ (var dst_line) (bv 32 0x4)) (cast 32 false (var word1))) (storew 0 (+ (var dst_line) (bv 32 0x8)) (cast 32 false (var word2))) (storew 0 (+ (var dst_line) (bv 32 0xc)) (cast 32 false (var word3))) (set a0 (cast 32 false (+ (var dst_addr) (bv 32 0x10)))))
d "move16 (a0), 0x1.l" f61000000001 0x0 (seq (set src_addr (cast 32 false (var a0))) (set dst_addr (cast 32 false (bv 32 0x1))) (set src_line (& (var src_addr) (bv 32 0xfffffff0))) (set dst_line (& (var dst_addr) (bv 32 0xfffffff0))) (set word0 (loadw 0 32 (var src_line))) (set word1 (loadw 0 32 (+ (var src_line) (bv 32 0x4)))) (set word2 (loadw 0 32 (+ (var src_line) (bv 32 0x8)))) (set word3 (loadw 0 32 (+ (var src_line) (bv 32 0xc)))) (storew 0 (var dst_line) (cast 32 false (var word0))) (storew 0 (+ (var dst_line) (bv 32 0x4)) (cast 32 false (var word1))) (storew 0 (+ (var dst_line) (bv 32 0x8)) (cast 32 false (var word2))) (storew 0 (+ (var dst_line) (bv 32 0xc)) (cast 32 false (var word3))))
d "move16 0x1.l, (a0)" f61800000001 0x0 (seq (set src_addr (cast 32 false (bv 32 0x1))) (set dst_addr (cast 32 false (var a0))) (set src_line (& (var src_addr) (bv 32 0xfffffff0))) (set dst_line (& (var dst_addr) (bv 32 0xfffffff0))) (set word0 (loadw 0 32 (var src_line))) (set word1 (loadw 0 32 (+ (var src_line) (bv 32 0x4)))) (set word2 (loadw 0 32 (+ (var src_line) (bv 32 0x8)))) (set word3 (loadw 0 32 (+ (var src_line) (bv 32 0xc)))) (storew 0 (var dst_line) (cast 32 false (var word0))) (storew 0 (+ (var dst_line) (bv 32 0x4)) (cast 32 false (var word1))) (storew 0 (+ (var dst_line) (bv 32 0x8)) (cast 32 false (var word2))) (storew 0 (+ (var dst_line) (bv 32 0xc)) (cast 32 false (var word3))))
d "move16 (a0)+, (a0)+" f6208000 0x0 (seq (set src_addr (var a0)) (set dst_addr (var a0)) (set src_line (& (var src_addr) (bv 32 0xfffffff0))) (set dst_line (& (var dst_addr) (bv 32 0xfffffff0))) (set word0 (loadw 0 32 (var src_line))) (set word1 (loadw 0 32 (+ (var src_line) (bv 32 0x4)))) (set word2 (loadw 0 32 (+ (var src_line) (bv 32 0x8)))) (set word3 (loadw 0 32 (+ (var src_line) (bv 32 0xc)))) (storew 0 (var dst_line) (cast 32 false (var word0))) (storew 0 (+ (var dst_line) (bv 32 0x4)) (cast 32 false (var word1))) (storew 0 (+ (var dst_line) (bv 32 0x8)) (cast 32 false (var word2))) (storew 0 (+ (var dst_line) (bv 32 0xc)) (cast 32 false (var word3))) (set a0 (cast 32 false (+ (var src_addr) (bv 32 0x10)))))
d "rte" 4e73 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set rte_state (bv 8 0x1)) (set target (bv 32 0x0)) (repeat (== (var rte_state) (bv 8 0x1)) (seq (set frame (var a7)) (set new_sr (loadw 0 16 (var frame))) (set target (loadw 0 32 (+ (var frame) (bv 32 0x2)))) (set format (>> (loadw 0 16 (+ (var frame) (bv 32 0x6))) (bv 8 0xc) false)) (set frame_size (ite (== (var format) (bv 16 0x0)) (bv 32 0x8) (ite (== (var format) (bv 16 0x1)) (bv 32 0x8) (ite (== (var format) (bv 16 0x2)) (bv 32 0xc) (ite (== (var format) (bv 16 0x3)) (bv 32 0xc) (ite (== (var format) (bv 16 0x4)) (bv 32 0x10) (ite (== (var format) (bv 16 0x7)) (bv 32 0x3c) (ite (== (var format) (bv 16 0x8)) (bv 32 0x3a) (ite (== (var format) (bv 16 0x9)) (bv 32 0x14) (ite (== (var format) (bv 16 0xa)) (bv 32 0x20) (bv 32 0x5c))))))))))) (branch (|| (&& (ule (var format) (bv 16 0x5)) (! (== (var format) (bv 16 0x5)))) (== (var format) (bv 16 0x7))) (seq (set a7 (cast 32 false (+ (var frame) (var frame_size)))) (set sr_write_value (cast 16 false (var new_sr))) (branch (! (== (ite (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000))) (bv 8 0x0) (ite (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x1000)))) (bv 8 0x2) (bv 8 0x1))) (ite (is_zero (& (var sr_write_value) (bv 16 0x2000))) (bv 8 0x0) (ite (! (is_zero (& (var sr_write_value) (bv 16 0x1000)))) (bv 8 0x2) (bv 8 0x1))))) (seq (branch (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000))) (set usp (cast 32 false (var a7))) (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x1000)))) (set msp (cast 32 false (var a7))) (set isp (cast 32 false (var a7))))) (branch (is_zero (& (var sr_write_value) (bv 16 0x2000))) (set a7 (cast 32 false (var usp))) (branch (! (is_zero (& (var sr_write_value) (bv 16 0x1000)))) (set a7 (cast 32 false (var msp))) (set a7 (cast 32 false (var isp)))))) empty) (set sr (var sr_write_value)) (set rte_state (ite (== (var format) (bv 16 0x1)) (bv 8 0x1) (bv 8 0x0)))) (set rte_state (bv 8 0x2))))) (branch (== (var rte_state) (bv 8 0x0)) (jmp (var target)) (seq (set trap_op (bv 32 0xa)) (set trap_vector (bv 32 0xe)) (goto m68k_trap)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "movem.l a0, -(a0)" 48e00080 0x0 (seq (set addr (var a0)) (set addr (- (var addr) (bv 32 0x4))) (storew 0 (var addr) (cast 32 false (cast 32 false (- (var a0) (bv 32 0x4))))) (set a0 (cast 32 false (var addr))))
d "fmove.x 0e1, fp0" f23c48003fff00008000000000000000
d "fmove.p 0e1.2345678901234567e+025, fp0" f23c4c00002500012345678901234567
d "fmove.p (a0), fp0" f2104c00
d "fmove.p fp0, (a1){-5}" f2116c7b
d "fmove.p fp2, (a2){d3}" f2127d30
d "fmove.p (a0)+, fp0" f2184c00
d "fmove.p fp0, -(a0){17}" f2206c11
