d "bgnd" 4afa 0x0 (seq (set trap_op (bv 32 0x5)) (goto m68k_trap))
d "lpstop 0x0" f80001c00000 0x0 (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege))
d "fbf.w 0x3" f2800001
d "fbeq.w 0x2" f2810000
d "fbogt.w 0x2" f2820000
d "fboge.w 0x2" f2830000
d "fbolt.w 0x2" f2840000
d "fbole.w 0x2" f2850000
d "fbogl.w 0x2" f2860000
d "fbor.w 0x2" f2870000
d "fbun.w 0x2" f2880000
d "fbueq.w 0x2" f2890000
d "fbugt.w 0x2" f28a0000
d "fbuge.w 0x2" f28b0000
d "fbult.w 0x2" f28c0000
d "fbule.w 0x2" f28d0000
d "fbne.w 0x2" f28e0000
d "fbt.w 0x2" f28f0000
d "fbf.l 0x3" f2c000000001
d "fbeq.l 0x3" f2c100000001
d "fbogt.l 0x3" f2c200000001
d "fboge.l 0x3" f2c300000001
d "fbolt.l 0x3" f2c400000001
d "fbole.l 0x3" f2c500000001
d "fbogl.l 0x3" f2c600000001
d "fbor.l 0x3" f2c700000001
d "fbun.l 0x3" f2c800000001
d "fbueq.l 0x3" f2c900000001
d "fbugt.l 0x3" f2ca00000001
d "fbuge.l 0x3" f2cb00000001
d "fbult.l 0x3" f2cc00000001
d "fbule.l 0x3" f2cd00000001
d "fbne.l 0x3" f2ce00000001
d "fbt.l 0x3" f2cf00000001
d "tblu.b d0:d0, d0" f8000000 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set entry0 (cast 64 false (cast 8 false (var d0)))) (set entry1 (cast 64 false (cast 8 false (var d0)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.l d0:d0, d0" f8000080 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set entry0 (cast 64 false (var d0))) (set entry1 (cast 64 false (var d0))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.w d1:d2, d3" f8013042 0x0 (seq (set x (cast 16 false (var d3))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set entry0 (cast 64 false (cast 16 false (var d1)))) (set entry1 (cast 64 false (cast 16 false (var d2)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d3 (| (& (var d3) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tbls.b d4:d5, d6" f8046805 0x0 (seq (set x (cast 16 false (var d6))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set entry0 (cast 64 (msb (cast 8 false (var d4))) (cast 8 false (var d4)))) (set entry1 (cast 64 (msb (cast 8 false (var d5))) (cast 8 false (var d5)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d6 (| (& (var d6) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.b (a0), d0" f8100100 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w (a0), d0" f8100140 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l (a0), d0" f8100180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblun.b (a1), d2" f8112500 0x0 (seq (set x (cast 16 false (var d2))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a1))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set fixed (+ (<< (var entry0) (bv 8 0x8) false) (var prod))) (set res (cast 32 false (cast 16 false (var fixed)))) (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 (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 "tbls.l (a2), d3" f8123980 0x0 (seq (set x (cast 16 false (var d3))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a2))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 (msb (loadw 0 32 (var entry_addr))) (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 (msb (loadw 0 32 (+ (var entry_addr) (bv 32 0x4)))) (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d3 (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 "tblsn.w (a4), d5" f8145d40 0x0 (seq (set x (cast 16 false (var d5))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a4))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 (msb (loadw 0 16 (var entry_addr))) (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 (msb (loadw 0 16 (+ (var entry_addr) (bv 32 0x2)))) (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set fixed (+ (<< (var entry0) (bv 8 0x8) false) (var prod))) (set res (cast 32 (msb (cast 24 false (var fixed))) (cast 24 false (var fixed)))) (set d5 (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 "tblu.b (a0)+, d0" f8180100 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w (a0)+, d0" f818017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l (a0)+, d0" f8180180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b -(a0), d0" f8200100 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w -(a0), d0" f820017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l -(a0), d0" f8200180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set base (cast 32 false (var a0))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b 0x17f(a0), d0" f8280100017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x17f))))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x180(a0), d0" f828017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x180))))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l 0x1ff(a0), d0" f828018001ff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1ff))))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b ([0x18001ff, a0], 0x8000fff), d0" f8300100017f018001ff08000fff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (+ (loadw 0 32 (+ (var a0) (bv 32 0x18001ff))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w (d0.w), d0" f830017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (+ (cast 32 false (bv 32 0x0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l ([0x8000fff], 0x10001fff), d0" f830018001ff08000fff10001fff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x8000fff))) (bv 32 0x0)) (bv 32 0x10001fff)))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b 0x17f.w, d0" f8380100017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x17f))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x180.w, d0" f838017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x180))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l 0x1ff.w, d0" f838018001ff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x1ff))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b 0x17f0180.l, d0" f8390100017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x17f0180))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x18001ff.l, d0" f839017f018001ff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x18001ff))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l 0x1ff0800.l, d0" f839018001ff0800 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x1ff0800))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b 0x183(pc), d0" f83a0100017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x183))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x184(pc), d0" f83a017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x184))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l 0x203(pc), d0" f83a018001ff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (bv 32 0x203))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b ([0x1800203, pc], 0x8000fff), d0" f83b0100017f018001ff08000fff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x1800201))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x4(pc, d0.w), d0" f83b017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (bv 32 0x2) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l ([0x8001003], 0x10001fff), d0" f83b018001ff08000fff10001fff 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x8001001))) (bv 32 0x0)) (bv 32 0x10001fff)))) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "tblu.b 0x7f, d0" f83c0100017f 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (bv 32 0x5)) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x1)))) (set entry0 (cast 64 false (loadw 0 8 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 8 (+ (var entry_addr) (bv 32 0x1))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 8 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (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 8 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 8 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 "tblu.w 0x180, d0" f83c017f0180 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (bv 32 0x4)) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x2)))) (set entry0 (cast 64 false (loadw 0 16 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 16 (+ (var entry_addr) (bv 32 0x2))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 16 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (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 16 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 16 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 "tblu.l 0x1ff0800, d0" f83c018001ff0800 0x0 (seq (set x (cast 16 false (var d0))) (set frac (cast 64 false (& (var x) (bv 16 0xff)))) (set base (bv 32 0x4)) (set index (cast 32 false (>> (& (var x) (bv 16 0xff00)) (bv 8 0x8) false))) (set entry_addr (+ (var base) (* (var index) (bv 32 0x4)))) (set entry0 (cast 64 false (loadw 0 32 (var entry_addr)))) (set entry1 (cast 64 false (loadw 0 32 (+ (var entry_addr) (bv 32 0x4))))) (set diff (- (var entry1) (var entry0))) (set prod (* (var diff) (var frac))) (set res (cast 32 false (+ (var entry0) (sdiv (ite (msb (var prod)) (- (var prod) (bv 64 0x80)) (+ (var prod) (bv 64 0x80))) (bv 64 0x100))))) (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 "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 0xc)) (bv 32 0x18) (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 0x3)) (! (== (var format) (bv 16 0x3)))) (== (var format) (bv 16 0xc))) (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 0x0)))) (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 0x0)))) (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 0x0)))) (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 0x0)))) (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))))
