rizin/test/db/asm/m68k_68010_32

d "ori.w 0x0, d0" 00400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (| (var dst) (var src))) (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 "andi.w 0x0, d0" 02400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (& (var dst) (var src))) (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 "subi.w 0x0, d0" 04400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (- (var dst) (var src))) (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 (&& (! (== (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 "addi.w 0x0, d0" 06400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (+ (var dst) (var src))) (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 (&& (== (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 "btst.b 0x0, 0x5(pc)" 083a00000001 0x0 (seq (set bit (bv 8 0x0)) (set dst (loadw 0 8 (bv 32 0x5))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (& (& (cast 8 false (var sr)) (bv 8 0xfb)) (bv 8 0xfb)) (<< (ite (! (! (is_zero (& (var dst) (<< (bv 8 0x1) (cast 8 false (mod (cast 8 false (var bit)) (bv 8 0x8))) false))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)))))))
d "btst.b 0x0, 0x5(pc, d0.w)" 083b00000001 0x0 (seq (set bit (bv 8 0x0)) (set dst (loadw 0 8 (+ (bv 32 0x5) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (& (& (cast 8 false (var sr)) (bv 8 0xfb)) (bv 8 0xfb)) (<< (ite (! (! (is_zero (& (var dst) (<< (bv 8 0x1) (cast 8 false (mod (cast 8 false (var bit)) (bv 8 0x8))) false))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)))))))
d "eori.w 0x0, d0" 0a400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (^ (var dst) (var src))) (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 "cmpi.b 0x0, 0x5(pc)" 0c3a00000001 0x0 (seq (set src (bv 8 0x0)) (set dst_addr (cast 32 false (bv 32 0x5))) (set dst (loadw 0 8 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.b 0x0, 0x5(pc, d0.w)" 0c3b00000001 0x0 (seq (set src (bv 8 0x0)) (set dst_addr (cast 32 false (+ (bv 32 0x5) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 8 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.b 0xff, 0x4(pc, d0.w)" 0c3b00ff0100 0x0 (seq (set src (bv 8 0xff)) (set dst_addr (cast 32 false (+ (bv 32 0x4) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 8 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.b 0x0, ([0x1800203, pc], 0x8000fff)" 0c3b0100017f018001ff08000fff 0x0 (seq (set src (bv 8 0x0)) (set dst_addr (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x1800201))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set dst (loadw 0 8 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.w 0x0, d0" 0c400000 0x0 (seq (set src (bv 16 0x0)) (set dst (cast 16 false (var d0))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.w 0x0, 0x5(pc)" 0c7a00000001 0x0 (seq (set src (bv 16 0x0)) (set dst_addr (cast 32 false (bv 32 0x5))) (set dst (loadw 0 16 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.w 0x0, 0x5(pc, d0.w)" 0c7b00000001 0x0 (seq (set src (bv 16 0x0)) (set dst_addr (cast 32 false (+ (bv 32 0x5) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 16 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.w 0xff, 0x4(pc, d0.w)" 0c7b00ff0100 0x0 (seq (set src (bv 16 0xff)) (set dst_addr (cast 32 false (+ (bv 32 0x4) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 16 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.w 0x100, ([0x1800203, pc], 0x8000fff)" 0c7b0100017f018001ff08000fff 0x0 (seq (set src (bv 16 0x100)) (set dst_addr (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x1800201))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set dst (loadw 0 16 (var dst_addr))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.l 0x1, 0x16(pc)" 0cba000000010010 0x0 (seq (set src (bv 32 0x1)) (set dst_addr (cast 32 false (bv 32 0x16))) (set dst (loadw 0 32 (var dst_addr))) (set res (- (var dst) (var src))) (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.l 0x1, 0x16(pc, d0.w)" 0cbb000000010010 0x0 (seq (set src (bv 32 0x1)) (set dst_addr (cast 32 false (+ (bv 32 0x16) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 32 (var dst_addr))) (set res (- (var dst) (var src))) (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.l 0x8000ff, 0x6(pc, d0.w)" 0cbb008000ff0100 0x0 (seq (set src (bv 32 0x8000ff)) (set dst_addr (cast 32 false (+ (bv 32 0x6) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0)))))) (set dst (loadw 0 32 (var dst_addr))) (set res (- (var dst) (var src))) (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "cmpi.l 0xff0100, ([0x1800205, pc], 0x8000fff)" 0cbb00ff0100017f018001ff08000fff 0x0 (seq (set src (bv 32 0xff0100)) (set dst_addr (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x2) (bv 32 0x1800203))) (bv 32 0x0)) (bv 32 0x8000fff)))) (set dst (loadw 0 32 (var dst_addr))) (set res (- (var dst) (var src))) (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "moves.b (a0), d0" 0e100000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (var a0)))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, (a0)" 0e100800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (var a0)) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b (a0)+, d0" 0e180000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (var a0)))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1)))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, (a0)+" 0e180800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (var a0)) (cast 8 false (var src))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x1))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b -(a0), d0" 0e200000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (set src (loadw 0 8 (cast 32 false (var a0)))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, -(a0)" 0e200800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (set a0 (cast 32 false (- (var a0) (bv 32 0x1)))) (storew 0 (cast 32 false (var a0)) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b 0x1(a0), d0" 0e2800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1)))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, 0xfff(a0)" 0e2808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xfff)))) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b 0x1(a0, d0.w), d0" 0e3000000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))))))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, ([0x10001fff], 0x20002fff)" 0e3008000fff10001fff20002fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x10001fff))) (bv 32 0x0)) (bv 32 0x20002fff))) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b ([0x20002fff], 0x30003fff), d1" 0e3010001fff20002fff30003fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x20002fff))) (bv 32 0x0)) (bv 32 0x30003fff))))) (set d1 (| (& (var d1) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b (a0, a0.w), a0" 0e3080008100 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var a0))) (cast 16 false (var a0))))))) (set a0 (cast 32 false (cast 32 (msb (var src)) (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b 0x1.w, d0" 0e3800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (bv 32 0x1)))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, 0xfff.w" 0e3808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (bv 32 0xfff)) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b 0x10010.l, d0" 0e39000000010010 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 8 (cast 32 false (bv 32 0x10010)))) (set d0 (| (& (var d0) (bv 32 0xffffff00)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.b d0, 0xfff1000.l" 0e3908000fff1000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 8 false (var d0))) (storew 0 (cast 32 false (bv 32 0xfff1000)) (cast 8 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w (a0), d0" 0e500000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (var a0)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, (a0)" 0e500800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (var a0)) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w (a0)+, d0" 0e580000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (var a0)))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, (a0)+" 0e580800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (var a0)) (cast 16 false (var src))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x2))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w -(a0), d0" 0e600000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (set src (loadw 0 16 (cast 32 false (var a0)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, -(a0)" 0e600800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (set a0 (cast 32 false (- (var a0) (bv 32 0x2)))) (storew 0 (cast 32 false (var a0)) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w 0x1(a0), d0" 0e6800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1)))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, 0xfff(a0)" 0e6808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xfff)))) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w 0x1(a0, d0.w), d0" 0e7000000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))))))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, ([0x10001fff], 0x20002fff)" 0e7008000fff10001fff20002fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x10001fff))) (bv 32 0x0)) (bv 32 0x20002fff))) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w ([0x20002fff], 0x30003fff), d1" 0e7010001fff20002fff30003fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x20002fff))) (bv 32 0x0)) (bv 32 0x30003fff))))) (set d1 (| (& (var d1) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w (a0, a0.w), a0" 0e7080008100 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var a0))) (cast 16 false (var a0))))))) (set a0 (cast 32 false (cast 32 (msb (var src)) (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w 0x1.w, d0" 0e7800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (bv 32 0x1)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, 0xfff.w" 0e7808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (bv 32 0xfff)) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w 0x10010.l, d0" 0e79000000010010 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 16 (cast 32 false (bv 32 0x10010)))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var src))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.w d0, 0xfff1000.l" 0e7908000fff1000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (cast 16 false (var d0))) (storew 0 (cast 32 false (bv 32 0xfff1000)) (cast 16 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l (a0), d0" 0e900000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (var a0)))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, (a0)" 0e900800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (var a0)) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l (a0)+, d0" 0e980000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (var a0)))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4)))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, (a0)+" 0e980800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (var a0)) (cast 32 false (var src))) (set a0 (cast 32 false (+ (var a0) (bv 32 0x4))))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l -(a0), d0" 0ea00000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (set src (loadw 0 32 (cast 32 false (var a0)))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, -(a0)" 0ea00800 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (set a0 (cast 32 false (- (var a0) (bv 32 0x4)))) (storew 0 (cast 32 false (var a0)) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l 0x1(a0), d0" 0ea800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1)))))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, 0xfff(a0)" 0ea808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0xfff)))) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l 0x1(a0, d0.w), d0" 0eb000000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x1))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))))))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, ([0x10001fff], 0x20002fff)" 0eb008000fff10001fff20002fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x10001fff))) (bv 32 0x0)) (bv 32 0x20002fff))) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l ([0x20002fff], 0x30003fff), d1" 0eb010001fff20002fff30003fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (+ (+ (loadw 0 32 (+ (bv 32 0x0) (bv 32 0x20002fff))) (bv 32 0x0)) (bv 32 0x30003fff))))) (set d1 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l (a0, a0.w), a0" 0eb080008100 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (+ (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0))) (cast 32 (msb (cast 16 false (var a0))) (cast 16 false (var a0))))))) (set a0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l 0x1.w, d0" 0eb800000001 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (bv 32 0x1)))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, 0xfff.w" 0eb808000fff 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (bv 32 0xfff)) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l 0x10010.l, d0" 0eb9000000010010 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (loadw 0 32 (cast 32 false (bv 32 0x10010)))) (set d0 (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "moves.l d0, 0xfff1000.l" 0eb908000fff1000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (seq (set src (var d0)) (storew 0 (cast 32 false (bv 32 0xfff1000)) (cast 32 false (var src)))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "move.l 0x1.l, d0" 203900000001 0x0 (seq (set src (loadw 0 32 (bv 32 0x1))) (set d0 (cast 32 false (var src))) (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 src))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (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 "lea.l 0x0(a0), a0" 41e80000 0x0 (set a0 (cast 32 false (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0)))))
d "bkpt 0x0" 4848 0x0 (seq (set trap_op (bv 32 0x1)) (set trap_arg (bv 32 0x0)) (goto m68k_trap))
d "pea.l 0x0(a0)" 48680000 0x0 (seq (set push_value (+ (cast 32 false (var a0)) (cast 32 false (bv 32 0x0)))) (set a7 (cast 32 false (- (var a7) (bv 32 0x4)))) (storew 0 (var a7) (cast 32 false (var push_value))))
d "link.w a0, 0x0" 4e500000 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 0x0))) (set a7 (cast 32 false (var new_sp))))
d "unlk a0" 4e58 0x0 (seq (set a7 (cast 32 false (var a0))) (set old (loadw 0 32 (var a7))) (set a7 (cast 32 false (+ (var a7) (bv 32 0x4)))) (set a0 (cast 32 false (var old))))
d "rtd 0x0" 4e740000 0x0 (seq (set target (loadw 0 32 (var a7))) (set a7 (cast 32 false (+ (var a7) (bv 32 0x4)))) (jmp (var target)))
d "movec sfc, d0" 4e7a0000 0x0 (branch (! (is_zero (& (cast 16 false (var sr)) (bv 16 0x2000)))) (set d0 (cast 32 false (var sfc))) (seq (set trap_op (bv 32 0x9)) (set trap_vector (bv 32 0x8)) (goto m68k_privilege)))
d "jsr 0x1.l" 4eb900000001 0x0 (seq (set target (bv 32 0x1)) (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 (var target)))
d "addq.w 0x8, d0" 5040 0x0 (seq (set src (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set res (+ (var dst) (var src))) (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 (&& (== (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 "dbt d0, 0x2" 50c80000 0x0 (branch true empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "subq.w 0x8, d0" 5140 0x0 (seq (set src (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set res (- (var dst) (var src))) (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 (&& (! (== (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 "dbra d0, 0x2" 51c80000 0x0 (branch false empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbhi d0, 0x2" 52c80000 0x0 (branch (&& (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1))))) (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbls d0, 0x2" 53c80000 0x0 (branch (|| (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1)))) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbcc d0, 0x2" 54c80000 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbcs d0, 0x2" 55c80000 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbne d0, 0x2" 56c80000 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbeq d0, 0x2" 57c80000 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbvc d0, 0x2" 58c80000 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbvs d0, 0x2" 59c80000 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbpl d0, 0x2" 5ac80000 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbmi d0, 0x2" 5bc80000 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbge d0, 0x2" 5cc80000 0x0 (branch (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dblt d0, 0x2" 5dc80000 0x0 (branch (! (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dbgt d0, 0x2" 5ec80000 0x0 (branch (&& (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0)))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "dble d0, 0x2" 5fc80000 0x0 (branch (|| (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))) (! (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0))))) empty (seq (set dec (- (cast 16 false (var d0)) (bv 16 0x1))) (set d0 (| (& (var d0) (bv 32 0xffff0000)) (cast 32 false (var dec)))) (branch (! (== (var dec) (bv 16 0xffff))) (jmp (bv 32 0x2)) empty)))
d "bra.b 0x3" 6001 0x0 (jmp (bv 32 0x3))
d "bsr.b 0x3" 6101 0x0 (seq (set push_value (bv 32 0x2)) (set a7 (cast 32 false (- (var a7) (bv 32 0x4)))) (storew 0 (var a7) (cast 32 false (var push_value))) (jmp (bv 32 0x3)))
d "bhi.b 0x3" 6201 0x0 (branch (&& (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1))))) (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))))) (jmp (bv 32 0x3)) empty)
d "bls.b 0x3" 6301 0x0 (branch (|| (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1)))) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) (jmp (bv 32 0x3)) empty)
d "bcc.b 0x3" 6401 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1))))) (jmp (bv 32 0x3)) empty)
d "bcs.b 0x3" 6501 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x1)))) (jmp (bv 32 0x3)) empty)
d "bne.b 0x3" 6601 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) (jmp (bv 32 0x3)) empty)
d "beq.b 0x3" 6701 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))) (jmp (bv 32 0x3)) empty)
d "bvc.b 0x3" 6801 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2))))) (jmp (bv 32 0x3)) empty)
d "bvs.b 0x3" 6901 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (jmp (bv 32 0x3)) empty)
d "bpl.b 0x3" 6a01 0x0 (branch (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8))))) (jmp (bv 32 0x3)) empty)
d "bmi.b 0x3" 6b01 0x0 (branch (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (jmp (bv 32 0x3)) empty)
d "bge.b 0x3" 6c01 0x0 (branch (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0))) (jmp (bv 32 0x3)) empty)
d "blt.b 0x3" 6d01 0x0 (branch (! (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0)))) (jmp (bv 32 0x3)) empty)
d "bgt.b 0x3" 6e01 0x0 (branch (&& (! (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4))))) (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0)))) (jmp (bv 32 0x3)) empty)
d "ble.b 0x3" 6f01 0x0 (branch (|| (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x4)))) (! (== (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x8)))) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (bv 1 0x1) (bv 1 0x0))))) (jmp (bv 32 0x3)) empty)
d "moveq 0x0, d0" 7000 0x0 (seq (set res (bv 32 0x0)) (set d0 (cast 32 false (bv 32 0x0))) (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 "or.w d0, d0" 8040 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (| (var dst) (var src))) (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 "sub.w d0, d0" 9040 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (- (var dst) (var src))) (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 (&& (! (== (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 "cmp.w d0, d0" b040 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (- (var dst) (var src))) (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 (&& (! (== (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)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
d "eor.w d0, d0" b140 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (^ (var dst) (var src))) (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 "and.w d0, d0" c040 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (& (var dst) (var src))) (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 "mulu.w d0, d0" c0c0 0x0 (seq (set src (cast 16 false (var d0))) (set res (* (cast 32 false (cast 16 false (var d0))) (cast 32 false (var src)))) (set d0 (cast 32 false (* (cast 32 false (cast 16 false (var d0))) (cast 32 false (var src))))) (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 "muls.w d0, d0" c1c0 0x0 (seq (set src (cast 16 false (var d0))) (set res (* (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 (msb (var src)) (var src)))) (set d0 (cast 32 false (* (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 (msb (var src)) (var src))))) (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 "add.w d0, d0" d040 0x0 (seq (set src (cast 16 false (var d0))) (set dst (cast 16 false (var d0))) (set res (+ (var dst) (var src))) (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 (&& (== (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 "asr.w 0x8, d0" e040 0x0 (seq (set count (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set count8 (& (cast 8 false (var count)) (bv 8 0x3f))) (set res (>> (var dst) (var count8) (msb (var dst)))) (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 (&& (! (is_zero (var count8))) (|| (&& (|| (! (ule (var count8) (bv 8 0x10))) (== (var count8) (bv 8 0x10))) (msb (var dst))) (&& (&& (ule (var count8) (bv 8 0x10)) (! (== (var count8) (bv 8 0x10)))) (! (is_zero (& (>> (var dst) (- (var count8) (bv 8 0x1)) false) (bv 16 0x1))))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (|| (&& (is_zero (var count8)) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x10))))) (&& (! (is_zero (var count8))) (|| (&& (|| (! (ule (var count8) (bv 8 0x10))) (== (var count8) (bv 8 0x10))) (msb (var dst))) (&& (&& (ule (var count8) (bv 8 0x10)) (! (== (var count8) (bv 8 0x10)))) (! (is_zero (& (>> (var dst) (- (var count8) (bv 8 0x1)) false) (bv 16 0x1)))))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
d "lsr.w 0x8, d0" e048 0x0 (seq (set count (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set count8 (& (cast 8 false (var count)) (bv 8 0x3f))) (set res (>> (var dst) (var count8) false)) (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 (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (var count8) (bv 8 0x1)) false) (bv 16 0x1))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (|| (&& (is_zero (var count8)) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x10))))) (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (var count8) (bv 8 0x1)) false) (bv 16 0x1)))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
d "asl.w 0x8, d0" e140 0x0 (seq (set count (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set count8 (& (cast 8 false (var count)) (bv 8 0x3f))) (set res (<< (var dst) (var count8) false)) (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 (&& (|| (! (ule (var count8) (bv 8 0x1))) (== (var count8) (bv 8 0x1))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0xe) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x2))) (== (var count8) (bv 8 0x2))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0xd) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x3))) (== (var count8) (bv 8 0x3))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0xc) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x4))) (== (var count8) (bv 8 0x4))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0xb) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x5))) (== (var count8) (bv 8 0x5))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0xa) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x6))) (== (var count8) (bv 8 0x6))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x9) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x7))) (== (var count8) (bv 8 0x7))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x8) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x8))) (== (var count8) (bv 8 0x8))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x7) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x9))) (== (var count8) (bv 8 0x9))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x6) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xa))) (== (var count8) (bv 8 0xa))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x5) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xb))) (== (var count8) (bv 8 0xb))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x4) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xc))) (== (var count8) (bv 8 0xc))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x3) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xd))) (== (var count8) (bv 8 0xd))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x2) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xe))) (== (var count8) (bv 8 0xe))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x1) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0xf))) (== (var count8) (bv 8 0xf))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite (! (is_zero (& (>> (var dst) (bv 8 0x0) false) (bv 16 0x1)))) (bv 1 0x1) (bv 1 0x0)))))) (&& (|| (! (ule (var count8) (bv 8 0x10))) (== (var count8) (bv 8 0x10))) (! (== (ite (msb (var dst)) (bv 1 0x1) (bv 1 0x0)) (ite false (bv 1 0x1) (bv 1 0x0)))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (bv 8 0x10) (var count8)) false) (bv 16 0x1))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (|| (&& (is_zero (var count8)) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x10))))) (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (bv 8 0x10) (var count8)) false) (bv 16 0x1)))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
d "lsl.w 0x8, d0" e148 0x0 (seq (set count (bv 16 0x8)) (set dst (cast 16 false (var d0))) (set count8 (& (cast 8 false (var count)) (bv 8 0x3f))) (set res (<< (var dst) (var count8) false)) (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 (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (bv 8 0x10) (var count8)) false) (bv 16 0x1))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (bv 8 0xef)) (<< (ite (|| (&& (is_zero (var count8)) (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x10))))) (&& (! (is_zero (var count8))) (! (is_zero (& (>> (var dst) (- (bv 8 0x10) (var count8)) false) (bv 16 0x1)))))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false)))))))
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 (|| (== (var format) (bv 16 0x0)) (== (var format) (bv 16 0x8))) (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 (var a0))) (set a0 (cast 32 false (var addr))))
d "rtd 0x4" 4e740004 0x0 (seq (set target (loadw 0 32 (var a7))) (set a7 (cast 32 false (+ (var a7) (bv 32 0x8)))) (jmp (var target)))