d "adc #0x42" 6942 0x0 (seq (set src (bv 8 0x42)) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc 0x42" 6542 0x0 (seq (set src (load 0 (bv 16 0x42))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc 0x42,x" 7542 0x0 (seq (set src (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc 0xcafe" 6dfeca 0x0 (seq (set src (load 0 (bv 16 0xcafe))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc 0xcafe,x" 7dfeca 0x0 (seq (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc 0xcafe,y" 79feca 0x0 (seq (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc (0x42,x)" 6142 0x0 (seq (set src (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "adc (0x42),y" 7142 0x0 (seq (set src (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "and #0x42" 2942 0x0 (seq (set a (& (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and 0x42" 2542 0x0 (seq (set a (& (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and 0x42,x" 3542 0x0 (seq (set a (& (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and 0xcafe" 2dfeca 0x0 (seq (set a (& (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and 0xcafe,x" 3dfeca 0x0 (seq (set a (& (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and 0xcafe,y" 39feca 0x0 (seq (set a (& (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and (0x42,x)" 2142 0x0 (seq (set a (& (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "and (0x42),y" 3142 0x0 (seq (set a (& (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "asl a" 0a 0x0 (seq (set tmp (var a)) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (set a (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "asl 0x42" 0642 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "asl 0x42,x" 1642 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "asl 0xcafe" 0efeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "asl 0xcafe,x" 1efeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "bcc 0x02e4" 90d0 0x312 (branch (! (var C)) (jmp (bv 16 0x2e4)) nop)
d "bcs 0x02e4" b0d0 0x312 (branch (var C) (jmp (bv 16 0x2e4)) nop)
d "beq 0x02e4" f0d0 0x312 (branch (var Z) (jmp (bv 16 0x2e4)) nop)
d "bit 0x42" 2442 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set N (msb (var tmp))) (set V (msb (cast 7 false (var tmp)))) (set Z (is_zero (& (var tmp) (var a)))))
d "bit 0xcafe" 2cfeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set N (msb (var tmp))) (set V (msb (cast 7 false (var tmp)))) (set Z (is_zero (& (var tmp) (var a)))))
d "bmi 0x02e4" 30d0 0x312 (branch (var N) (jmp (bv 16 0x2e4)) nop)
d "bne 0x02e4" d0d0 0x312 (branch (! (var Z)) (jmp (bv 16 0x2e4)) nop)
d "bpl 0x02e4" 10d0 0x312 (branch (! (var N)) (jmp (bv 16 0x2e4)) nop)
d "brk" 00 0x2040 (seq (store 0 (append (bv 8 0x1) (var sp)) (bv 8 0x20)) (set sp (- (var sp) (bv 8 0x1))) (store 0 (append (bv 8 0x1) (var sp)) (bv 8 0x42)) (set sp (- (var sp) (bv 8 0x1))) (store 0 (append (bv 8 0x1) (var sp)) (| (| (ite (var N) (bv 8 0xb0) (bv 8 0x30)) (| (ite (var V) (bv 8 0x40) (bv 8 0x0)) (| (ite (var D) (bv 8 0x8) (bv 8 0x0)) (| (ite (var I) (bv 8 0x4) (bv 8 0x0)) (| (ite (var Z) (bv 8 0x2) (bv 8 0x0)) (ite (var C) (bv 8 0x1) (bv 8 0x0))))))) (bv 8 0x20))) (set sp (- (var sp) (bv 8 0x1))) (set D false) (set I true) (jmp (loadw 0 16 (bv 16 0xfffe))))
d "bvc 0x02e4" 50d0 0x312 (branch (! (var V)) (jmp (bv 16 0x2e4)) nop)
d "bvs 0x02e4" 70d0 0x312 (branch (var V) (jmp (bv 16 0x2e4)) nop)
d "clc" 18 0x0 (set C false)
d "cld" d8 0x0 (set D false)
d "cli" 58 0x0 (set I false)
d "clv" b8 0x0 (set V false)
d "cmp #0x42" c942 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (bv 8 0x42)))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp 0x42" c542 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (bv 16 0x42))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp 0x42,x" d542 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp 0xcafe" cdfeca 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (bv 16 0xcafe))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp 0xcafe,x" ddfeca 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp 0xcafe,y" d9feca 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp (0x42,x)" c142 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cmp (0x42),y" d142 0x0 (seq (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpx #0x42" e042 0x0 (seq (set cmptmp (- (cast 9 false (var x)) (cast 9 false (bv 8 0x42)))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpx 0x42" e442 0x0 (seq (set cmptmp (- (cast 9 false (var x)) (cast 9 false (load 0 (bv 16 0x42))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpx 0xcafe" ecfeca 0x0 (seq (set cmptmp (- (cast 9 false (var x)) (cast 9 false (load 0 (bv 16 0xcafe))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpy #0x42" c042 0x0 (seq (set cmptmp (- (cast 9 false (var y)) (cast 9 false (bv 8 0x42)))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpy 0x42" c442 0x0 (seq (set cmptmp (- (cast 9 false (var y)) (cast 9 false (load 0 (bv 16 0x42))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "cpy 0xcafe" ccfeca 0x0 (seq (set cmptmp (- (cast 9 false (var y)) (cast 9 false (load 0 (bv 16 0xcafe))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dec 0x42" c642 0x0 (seq (set tmp (- (load 0 (bv 16 0x42)) (bv 8 0x1))) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "dec 0x42,x" d642 0x0 (seq (set tmp (- (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))) (bv 8 0x1))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "dec 0xcafe" cefeca 0x0 (seq (set tmp (- (load 0 (bv 16 0xcafe)) (bv 8 0x1))) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "dec 0xcafe,x" defeca 0x0 (seq (set tmp (- (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "dex" ca 0x0 (seq (set x (- (var x) (bv 8 0x1))) (set Z (is_zero (cast 8 false (var x)))) (set N (msb (cast 8 false (var x)))))
d "dey" 88 0x0 (seq (set y (- (var y) (bv 8 0x1))) (set Z (is_zero (cast 8 false (var y)))) (set N (msb (cast 8 false (var y)))))
d "eor #0x42" 4942 0x0 (seq (set a (^ (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor 0x42" 4542 0x0 (seq (set a (^ (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor 0x42,x" 5542 0x0 (seq (set a (^ (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor 0xcafe" 4dfeca 0x0 (seq (set a (^ (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor 0xcafe,x" 5dfeca 0x0 (seq (set a (^ (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor 0xcafe,y" 59feca 0x0 (seq (set a (^ (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor (0x42,x)" 4142 0x0 (seq (set a (^ (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "eor (0x42),y" 5142 0x0 (seq (set a (^ (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "inc 0x42" e642 0x0 (seq (set tmp (+ (load 0 (bv 16 0x42)) (bv 8 0x1))) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "inc 0x42,x" f642 0x0 (seq (set tmp (+ (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))) (bv 8 0x1))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "inc 0xcafe" eefeca 0x0 (seq (set tmp (+ (load 0 (bv 16 0xcafe)) (bv 8 0x1))) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "inc 0xcafe,x" fefeca 0x0 (seq (set tmp (+ (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "inx" e8 0x0 (seq (set x (+ (var x) (bv 8 0x1))) (set Z (is_zero (cast 8 false (var x)))) (set N (msb (cast 8 false (var x)))))
d "iny" c8 0x0 (seq (set y (+ (var y) (bv 8 0x1))) (set Z (is_zero (cast 8 false (var y)))) (set N (msb (cast 8 false (var y)))))
d "jmp 0xcafe" 4cfeca 0x0 (jmp (bv 16 0xcafe))
d "jmp (0xcafe)" 6cfeca 0x0 (jmp (loadw 0 16 (bv 16 0xcafe)))
d "jsr 0xcafe" 20feca 0x3240 (seq (store 0 (append (bv 8 0x1) (var sp)) (bv 8 0x32)) (set sp (- (var sp) (bv 8 0x1))) (store 0 (append (bv 8 0x1) (var sp)) (bv 8 0x42)) (set sp (- (var sp) (bv 8 0x1))) (jmp (bv 16 0xcafe)))
d "lda #0x42" a942 0x0 (seq (set a (bv 8 0x42)) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda 0x42" a542 0x0 (seq (set a (load 0 (bv 16 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda 0x42,x" b542 0x0 (seq (set a (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda 0xcafe" adfeca 0x0 (seq (set a (load 0 (bv 16 0xcafe))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda 0xcafe,x" bdfeca 0x0 (seq (set a (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda 0xcafe,y" b9feca 0x0 (seq (set a (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda (0x42,x)" a142 0x0 (seq (set a (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "lda (0x42),y" b142 0x0 (seq (set a (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ldx #0x42" a242 0x0 (seq (set x (bv 8 0x42)) (set Z (is_zero (var x))) (set N (msb (var x))))
d "ldx 0x42" a642 0x0 (seq (set x (load 0 (bv 16 0x42))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "ldx 0x42,y" b642 0x0 (seq (set x (load 0 (cast 16 false (+ (bv 8 0x42) (var y))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "ldx 0xcafe" aefeca 0x0 (seq (set x (load 0 (bv 16 0xcafe))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "ldx 0xcafe,y" befeca 0x0 (seq (set x (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "ldy #0x42" a042 0x0 (seq (set y (bv 8 0x42)) (set Z (is_zero (var y))) (set N (msb (var y))))
d "ldy 0x42" a442 0x0 (seq (set y (load 0 (bv 16 0x42))) (set Z (is_zero (var y))) (set N (msb (var y))))
d "ldy 0x42,x" b442 0x0 (seq (set y (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set Z (is_zero (var y))) (set N (msb (var y))))
d "ldy 0xcafe" acfeca 0x0 (seq (set y (load 0 (bv 16 0xcafe))) (set Z (is_zero (var y))) (set N (msb (var y))))
d "ldy 0xcafe,x" bcfeca 0x0 (seq (set y (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set Z (is_zero (var y))) (set N (msb (var y))))
d "lsr a" 4a 0x0 (seq (set tmp (var a)) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (set a (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "lsr 0x42" 4642 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "lsr 0x42,x" 5642 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "lsr 0xcafe" 4efeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "lsr 0xcafe,x" 5efeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "nop" ea 0x0 nop
d "ora #0x42" 0942 0x0 (seq (set a (| (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora 0x42" 0542 0x0 (seq (set a (| (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora 0x42,x" 1542 0x0 (seq (set a (| (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora 0xcafe" 0dfeca 0x0 (seq (set a (| (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora 0xcafe,x" 1dfeca 0x0 (seq (set a (| (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora 0xcafe,y" 19feca 0x0 (seq (set a (| (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora (0x42,x)" 0142 0x0 (seq (set a (| (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "ora (0x42),y" 1142 0x0 (seq (set a (| (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "pha" 48 0x0 (seq (store 0 (append (bv 8 0x1) (var sp)) (var a)) (set sp (- (var sp) (bv 8 0x1))))
d "php" 08 0x0 (seq (store 0 (append (bv 8 0x1) (var sp)) (| (| (ite (var N) (bv 8 0xb0) (bv 8 0x30)) (| (ite (var V) (bv 8 0x40) (bv 8 0x0)) (| (ite (var D) (bv 8 0x8) (bv 8 0x0)) (| (ite (var I) (bv 8 0x4) (bv 8 0x0)) (| (ite (var Z) (bv 8 0x2) (bv 8 0x0)) (ite (var C) (bv 8 0x1) (bv 8 0x0))))))) (bv 8 0x20))) (set sp (- (var sp) (bv 8 0x1))))
d "pla" 68 0x0 (seq (set sp (+ (var sp) (bv 8 0x1))) (set tmp (load 0 (append (bv 8 0x1) (var sp)))) (set a (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))))
d "plp" 28 0x0 (seq (set sp (+ (var sp) (bv 8 0x1))) (set tmp (load 0 (append (bv 8 0x1) (var sp)))) (set N (msb (var tmp))) (set V (! (is_zero (& (var tmp) (bv 8 0x40))))) (set D (! (is_zero (& (var tmp) (bv 8 0x8))))) (set I (! (is_zero (& (var tmp) (bv 8 0x4))))) (set Z (! (is_zero (& (var tmp) (bv 8 0x2))))) (set C (lsb (var tmp))))
d "rol a" 2a 0x0 (seq (set tmp (var a)) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (set a (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "rol 0x42" 2642 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (bv 16 0x42) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "rol 0x42,x" 3642 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "rol 0xcafe" 2efeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (bv 16 0xcafe) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "rol 0xcafe,x" 3efeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "ror a" 6a 0x0 (seq (set tmp (var a)) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (set a (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "ror 0x42" 6642 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (bv 16 0x42) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "ror 0x42,x" 7642 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "ror 0xcafe" 6efeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (bv 16 0xcafe) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "ror 0xcafe,x" 7efeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "rti" 40 0x0 (seq (set sp (+ (var sp) (bv 8 0x1))) (set sr (load 0 (append (bv 8 0x1) (var sp)))) (set N (msb (var sr))) (set V (! (is_zero (& (var sr) (bv 8 0x40))))) (set D (! (is_zero (& (var sr) (bv 8 0x8))))) (set I (! (is_zero (& (var sr) (bv 8 0x4))))) (set Z (! (is_zero (& (var sr) (bv 8 0x2))))) (set C (lsb (var sr))) (set sp (+ (var sp) (bv 8 0x1))) (set pcl (load 0 (append (bv 8 0x1) (var sp)))) (set sp (+ (var sp) (bv 8 0x1))) (set pch (load 0 (append (bv 8 0x1) (var sp)))) (jmp (append (var pch) (var pcl))))
d "rts" 60 0x0 (seq (set sp (+ (var sp) (bv 8 0x1))) (set pcl (load 0 (append (bv 8 0x1) (var sp)))) (set sp (+ (var sp) (bv 8 0x1))) (set pch (load 0 (append (bv 8 0x1) (var sp)))) (jmp (+ (append (var pch) (var pcl)) (bv 16 0x1))))
d "sbc #0x42" e942 0x0 (seq (set src (bv 8 0x42)) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc 0x42" e542 0x0 (seq (set src (load 0 (bv 16 0x42))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc 0x42,x" f542 0x0 (seq (set src (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc 0xcafe" edfeca 0x0 (seq (set src (load 0 (bv 16 0xcafe))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc 0xcafe,x" fdfeca 0x0 (seq (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc 0xcafe,y" f9feca 0x0 (seq (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc (0x42,x)" e142 0x0 (seq (set src (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sbc (0x42),y" f142 0x0 (seq (set src (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "sec" 38 0x0 (set C true)
d "sed" f8 0x0 (set D true)
d "sei" 78 0x0 (set I true)
d "sta 0x42" 8542 0x0 (store 0 (bv 16 0x42) (var a))
d "sta 0x42,x" 9542 0x0 (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var a))
d "sta 0xcafe" 8dfeca 0x0 (store 0 (bv 16 0xcafe) (var a))
d "sta 0xcafe,x" 9dfeca 0x0 (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var a))
d "sta 0xcafe,y" 99feca 0x0 (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var a))
d "sta (0x42,x)" 8142 0x0 (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var a))
d "sta (0x42),y" 9142 0x0 (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var a))
d "stx 0x42" 8642 0x0 (store 0 (bv 16 0x42) (var x))
d "stx 0x42,y" 9642 0x0 (store 0 (cast 16 false (+ (bv 8 0x42) (var y))) (var x))
d "stx 0xcafe" 8efeca 0x0 (store 0 (bv 16 0xcafe) (var x))
d "sty 0x42" 8442 0x0 (store 0 (bv 16 0x42) (var y))
d "sty 0x42,x" 9442 0x0 (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var y))
d "sty 0xcafe" 8cfeca 0x0 (store 0 (bv 16 0xcafe) (var y))
d "tax" aa 0x0 (seq (set x (var a)) (set Z (is_zero (var x))) (set N (msb (var x))))
d "tay" a8 0x0 (seq (set y (var a)) (set Z (is_zero (var y))) (set N (msb (var y))))
d "tsx" ba 0x0 (seq (set x (var sp)) (set Z (is_zero (var x))) (set N (msb (var x))))
d "txa" 8a 0x0 (seq (set a (var x)) (set Z (is_zero (var a))) (set N (msb (var a))))
d "txs" 9a 0x0 (set sp (var x))
d "tya" 98 0x0 (seq (set a (var y)) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo 0x42" 0742 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo 0x42,x" 1742 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo (0x42,x)" 0342 0x0 (seq (set tmp (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo (0x42),y" 1342 0x0 (seq (set tmp (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo 0xcafe" 0ffeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo 0xcafe,x" 1ffeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "slo 0xcafe,y" 1bfeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set C (msb (var tmp))) (set tmp (<< (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set a (| (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla 0x42" 2742 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (bv 16 0x42) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla 0x42,x" 3742 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla (0x42,x)" 2342 0x0 (seq (set tmp (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla (0x42),y" 3342 0x0 (seq (set tmp (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla 0xcafe" 2ffeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (bv 16 0xcafe) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla 0xcafe,y" 3bfeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rla 0xcafe,x" 3ffeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (| (<< (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x1) (bv 8 0x0)))) (set C (msb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set a (& (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre 0x42" 4742 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (bv 16 0x42)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre 0x42,x" 5742 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre (0x42,x)" 4342 0x0 (seq (set tmp (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre (0x42),y" 5342 0x0 (seq (set tmp (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre 0xcafe" 4ffeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (bv 16 0xcafe)))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre 0xcafe,y" 5bfeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "sre 0xcafe,x" 5ffeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N false) (set a (^ (var a) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "rra 0x42" 6742 0x0 (seq (set tmp (load 0 (bv 16 0x42))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (bv 16 0x42) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (bv 16 0x42))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra 0x42,x" 7742 0x0 (seq (set tmp (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra (0x42,x)" 6342 0x0 (seq (set tmp (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra (0x42),y" 7342 0x0 (seq (set tmp (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra 0xcafe" 6ffeca 0x0 (seq (set tmp (load 0 (bv 16 0xcafe))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (bv 16 0xcafe) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (bv 16 0xcafe))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra 0xcafe,x" 7ffeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "rra 0xcafe,y" 7bfeca 0x0 (seq (set tmp (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var res)) (set Z (is_zero (var res))) (set N (msb (var res))) (set src (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set res (+ (ite (var C) (bv 8 0x1) (bv 8 0x0)) (+ (var a) (var src)))) (set Z (is_zero (var res))) (set N (msb (var res))) (set C (ite (var C) (ule (var res) (var a)) (&& (ule (var res) (var a)) (! (== (var res) (var a)))))) (set V (&& (! (^^ (msb (var a)) (msb (var src)))) (^^ (msb (var a)) (msb (var res))))) (set a (var res)))
d "sax 0x42" 8742 0x0 (store 0 (bv 16 0x42) (& (var a) (var x)))
d "sax 0x42,y" 9742 0x0 (store 0 (cast 16 false (+ (bv 8 0x42) (var y))) (& (var a) (var x)))
d "sax (0x42,x)" 8342 0x0 (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (& (var a) (var x)))
d "sax 0xcafe" 8ffeca 0x0 (store 0 (bv 16 0xcafe) (& (var a) (var x)))
d "lax 0x42" a742 0x0 (seq (set a (load 0 (bv 16 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (bv 16 0x42))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lax 0x42,y" b742 0x0 (seq (set a (load 0 (cast 16 false (+ (bv 8 0x42) (var y))))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (cast 16 false (+ (bv 8 0x42) (var y))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lax (0x42,x)" a342 0x0 (seq (set a (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lax (0x42),y" b342 0x0 (seq (set a (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lax 0xcafe" affeca 0x0 (seq (set a (load 0 (bv 16 0xcafe))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (bv 16 0xcafe))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lax 0xcafe,y" bffeca 0x0 (seq (set a (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set Z (is_zero (var a))) (set N (msb (var a))) (set x (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lxa #0x42" ab42 0x0 (seq (set a (& (| (var a) (bv 8 0xee)) (cast 8 false (bv 8 0x42)))) (set x (var a)) (set Z (is_zero (var a))) (set N (msb (var a))))
d "dcp 0x42" c742 0x0 (seq (set tmp (- (load 0 (bv 16 0x42)) (bv 8 0x1))) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (bv 16 0x42))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp 0x42,x" d742 0x0 (seq (set tmp (- (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))) (bv 8 0x1))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp (0x42,x)" c342 0x0 (seq (set tmp (- (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (bv 8 0x1))) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp (0x42),y" d342 0x0 (seq (set tmp (- (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))) (bv 8 0x1))) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp 0xcafe" cffeca 0x0 (seq (set tmp (- (load 0 (bv 16 0xcafe)) (bv 8 0x1))) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (bv 16 0xcafe))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp 0xcafe,x" dffeca 0x0 (seq (set tmp (- (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (bv 16 0xcafe) (cast 16 false (var x))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "dcp 0xcafe,y" dbfeca 0x0 (seq (set tmp (- (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set cmptmp (- (cast 9 false (var a)) (cast 9 false (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y))))))) (set C (! (msb (var cmptmp)))) (set Z (is_zero (cast 8 false (var cmptmp)))) (set N (msb (cast 8 false (var cmptmp)))))
d "isb 0x42" e742 0x0 (seq (set tmp (+ (load 0 (bv 16 0x42)) (bv 8 0x1))) (store 0 (bv 16 0x42) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (bv 16 0x42))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb 0x42,x" f742 0x0 (seq (set tmp (+ (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))) (bv 8 0x1))) (store 0 (cast 16 false (+ (bv 8 0x42) (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb (0x42,x)" e342 0x0 (seq (set tmp (+ (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x)))))) (bv 8 0x1))) (store 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (append (load 0 (cast 16 false (+ (+ (bv 8 0x42) (var x)) (bv 8 0x1)))) (load 0 (cast 16 false (+ (bv 8 0x42) (var x))))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb (0x42),y" f342 0x0 (seq (set tmp (+ (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y)))) (bv 8 0x1))) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb 0xcafe" effeca 0x0 (seq (set tmp (+ (load 0 (bv 16 0xcafe)) (bv 8 0x1))) (store 0 (bv 16 0xcafe) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (bv 16 0xcafe))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb 0xcafe,x" fffeca 0x0 (seq (set tmp (+ (load 0 (+ (bv 16 0xfe) (cast 16 false (var x)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xfe) (cast 16 false (var x))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (+ (bv 16 0xfe) (cast 16 false (var x))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "isb 0xcafe,y" fbfeca 0x0 (seq (set tmp (+ (load 0 (+ (bv 16 0xfe) (cast 16 false (var y)))) (bv 8 0x1))) (store 0 (+ (bv 16 0xfe) (cast 16 false (var y))) (var tmp)) (set Z (is_zero (var tmp))) (set N (msb (var tmp))) (set src (load 0 (+ (bv 16 0xfe) (cast 16 false (var y))))) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)))
d "anc #0x42" 0b42 0x0 (seq (set a (& (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))) (set C (msb (var a))))
d "anc #0x42" 2b42 0x0 (seq (set a (& (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))) (set C (msb (var a))))
d "asr #0x42" 4b42 0x0 (seq (set a (& (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))) (set tmp (var a)) (set C (lsb (var tmp))) (set tmp (>> (var tmp) (bv 3 0x1) false)) (set a (var tmp)) (set Z (is_zero (var tmp))) (set N false))
d "arr #0x42" 6b42 0x0 (seq (set a (& (var a) (bv 8 0x42))) (set Z (is_zero (var a))) (set N (msb (var a))) (set tmp (var a)) (set res (| (>> (var tmp) (bv 3 0x1) false) (ite (var C) (bv 8 0x80) (bv 8 0x0)))) (set C (lsb (var tmp))) (set a (var res)) (set Z (is_zero (var res))) (set N (msb (var res))))
d "sbx 0x42" cb42 0x0 (seq (set tmp (bv 8 0x42)) (set ax (& (var a) (var x))) (set ax (- (var ax) (var tmp))) (set x (var ax)) (set Z (is_zero (var x))) (set N (msb (var x))))
d "lae 0xcafe,y" bbfeca 0x0 (seq (set sp (& (var sp) (load 0 (+ (bv 16 0xcafe) (cast 16 false (var y)))))) (set Z (is_zero (var sp))) (set N (msb (var sp))) (set x (var sp)) (set a (var sp)))
d "hlt" 02 0x0 empty
d "hlt" 12 0x0 empty
d "hlt" 22 0x0 empty
d "hlt" 32 0x0 empty
d "hlt" 42 0x0 empty
d "hlt" 52 0x0 empty
d "hlt" 62 0x0 empty
d "hlt" 72 0x0 empty
d "hlt" 92 0x0 empty
d "sha (0x0042),y" 9342 0x0 (seq (set tmp (& (& (var a) (var x)) (+ (cast 8 false (>> (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (bv 8 0x8) false)) (bv 8 0x1)))) (store 0 (+ (append (load 0 (cast 16 false (+ (bv 8 0x42) (bv 8 0x1)))) (load 0 (cast 16 false (bv 8 0x42)))) (cast 16 false (var y))) (var tmp)))
d "hlt" b2 0x0 empty
d "hlt" d2 0x0 empty
d "hlt" f2 0x0 empty
d "sha 0xcafe,y" 9ffeca 0x0 (seq (set tmp (& (& (var a) (var x)) (+ (cast 8 false (>> (+ (bv 16 0xcafe) (cast 16 false (var y))) (bv 8 0x8) false)) (bv 8 0x1)))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)))
d "shx 0xcafe,y" 9efeca 0x0 (seq (set tmp (& (var x) (+ (cast 8 false (>> (+ (bv 16 0xcafe) (cast 16 false (var y))) (bv 8 0x8) false)) (bv 8 0x1)))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)))
d "shy 0xcafe,x" 9cfeca 0x0 (seq (set tmp (& (var y) (+ (cast 8 false (>> (+ (bv 16 0xcafe) (cast 16 false (var x))) (bv 8 0x8) false)) (bv 8 0x1)))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var x))) (var tmp)))
d "shs 0xcafe,y" 9bfeca 0x0 (seq (set sp (& (var a) (var x))) (set tmp (& (& (var a) (var x)) (+ (cast 8 false (>> (+ (bv 16 0xcafe) (cast 16 false (var y))) (bv 8 0x8) false)) (bv 8 0x1)))) (store 0 (+ (bv 16 0xcafe) (cast 16 false (var y))) (var tmp)))
d "ane #0x42" 8b42 0x0 (seq (set a (& (| (var a) (bv 8 0xee)) (& (var x) (cast 8 false (bv 8 0x42))))) (set Z (is_zero (var a))) (set N (msb (var a))))
d "nop #0x42" 8042 0x0 nop
d "nop #0x42" 8242 0x0 nop
d "nop #0x42" c242 0x0 nop
d "nop #0x42" e242 0x0 nop
d "nop #0x42" 8942 0x0 nop
d "nop 0x42" 0442 0x0 nop
d "nop 0x42" 4442 0x0 nop
d "nop 0x42" 6442 0x0 nop
d "nop 0xcafe,x" 1cfeca 0x0 nop
d "nop 0xcafe,x" 3cfeca 0x0 nop
d "nop 0xcafe,x" 5cfeca 0x0 nop
d "nop 0xcafe,x" 7cfeca 0x0 nop
d "nop 0xcafe,x" dcfeca 0x0 nop
d "nop 0xcafe,x" fcfeca 0x0 nop
d "nop 0x42,x" 1442 0x0 nop
d "nop 0x42,x" 3442 0x0 nop
d "nop 0x42,x" 5442 0x0 nop
d "nop 0x42,x" 7442 0x0 nop
d "nop 0x42,x" d442 0x0 nop
d "nop 0x42,x" f442 0x0 nop
d "invalid" ff 0x0
d "invalid" bb 0x0
d "sbc #0x42" eb42 0x0 (seq (set src (bv 8 0x42)) (set res (- (- (cast 9 false (var a)) (cast 9 false (var src))) (ite (var C) (bv 9 0x0) (bv 9 0x1)))) (set C (! (msb (var res)))) (set res8 (cast 8 false (var res))) (set Z (is_zero (var res8))) (set N (msb (var res8))) (set V (&& (^^ (msb (var a)) (msb (var res8))) (^^ (msb (var a)) (msb (var src))))) (set a (var res8)));empty
d "nop 0x3412" 0c1234 0x0 nop
