dE "add g1, g2, g3" 86004002 0x0 (set g3 (+ (cast 64 false (var g1)) (cast 64 false (var g2))))
dE "sub g1, g2, g3" 86204002 0x0 (set g3 (- (cast 64 false (var g1)) (cast 64 false (var g2))))
dE "addcc g1, g2, g3" 86804002 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g1)))) (set arg1 (cast 128 false (cast 64 false (var g2)))) (set res128_mid (+ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (! (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1))))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (! (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1))))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (^^ (^^ (msb (cast 33 false (var arg0))) (msb (cast 33 false (var arg1)))) (msb (cast 33 false (var res128))))) (set carry64 (msb (cast 65 false (var res128)))) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "subcc g1, g2, g3" 86a04002 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g1)))) (set arg1 (cast 128 false (cast 64 false (var g2)))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "addx g2, g1, g3" 86408001 0x0 (set g3 (+ (+ (cast 64 false (var g2)) (cast 64 false (var g1))) (ite (lsb (var ccr)) (bv 64 0x1) (bv 64 0x0))))
dE "subx g2, g1, g3" 86608001 0x0 (set g3 (- (- (cast 64 false (var g2)) (cast 64 false (var g1))) (ite (lsb (var ccr)) (bv 64 0x1) (bv 64 0x0))))
dE "udiv g1, g2, g3" 86704002 0x0 (seq (set res128 (cast 128 false (div (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g1)))) (cast 64 false (cast 64 false (var g2)))))) (set g3 (cast 64 false (var res128))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 64 0x7fffffff) (cast 64 false (var res128)))))
dE "sdiv g1, g2, g3" 86784002 0x0 (seq (set res128 (cast 128 (msb (sdiv (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g1)))) (cast 64 (msb (cast 32 false (cast 64 false (var g2)))) (cast 32 false (cast 64 false (var g2)))))) (sdiv (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g1)))) (cast 64 (msb (cast 32 false (cast 64 false (var g2)))) (cast 32 false (cast 64 false (var g2))))))) (set g3 (cast 64 (msb (var res128)) (var res128))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 64 0x7fffffff) (ite (sle (var res128) (bv 128 0xffffffffffffffffffffffff80000001)) (bv 64 0xffffffff80000000) (cast 64 (msb (var res128)) (var res128))))))
dE "umul g1, g2, g3" 86504002 0x0 (seq (set res128 (* (cast 64 false (cast 32 false (cast 64 false (var g1)))) (cast 64 false (cast 32 false (cast 64 false (var g2)))))) (set g3 (cast 64 false (var res128))) (set y (cast 64 false (>> (var res128) (bv 8 0x20) false))))
dE "smul g1, g2, g3" 86584002 0x0 (seq (set res128 (* (cast 64 (msb (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1)))) (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1)))) (cast 64 (msb (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2)))) (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2)))))) (set g3 (cast 64 false (var res128))) (set y (cast 64 false (>> (var res128) (bv 8 0x20) false))))
dE "umulcc g2, g1, g3" 86d08001 0x0 (seq (set arg0 (cast 128 (msb (cast 64 false (cast 32 false (cast 64 false (var g2))))) (cast 64 false (cast 32 false (cast 64 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 false (cast 32 false (cast 64 false (var g1))))) (cast 64 false (cast 32 false (cast 64 false (var g1)))))) (set res128_mid (* (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))) (set y (cast 64 false (>> (var res128) (bv 8 0x20) false))))
dE "smulcc g2, g1, g3" 86d88001 0x0 (seq (set arg0 (cast 128 (msb (cast 64 (msb (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2)))) (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2))))) (cast 64 (msb (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2)))) (cast 32 (msb (cast 64 false (var g2))) (cast 64 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 (msb (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1)))) (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1))))) (cast 64 (msb (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1)))) (cast 32 (msb (cast 64 false (var g1))) (cast 64 false (var g1)))))) (set res128_mid (* (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))) (set y (cast 64 false (>> (var res128) (bv 8 0x20) false))))
dE "udivcc g2, g1, g3" 86f08001 0x0 (seq (set arg0 (cast 128 false (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g2)))))) (set arg1 (cast 128 false (cast 64 false (cast 64 false (var g1))))) (set res128_mid (div (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (|| (! (ule (var res128) (bv 128 0x100000000))) (== (var res128) (bv 128 0x100000000)))) empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 64 0x7fffffff) (cast 64 false (var res128)))))
dE "sdivcc g2, g1, g3" 86f88001 0x0 (seq (set arg0 (cast 128 (msb (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g2))))) (append (cast 32 false (var y)) (cast 32 false (cast 64 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 (msb (cast 32 false (cast 64 false (var g1)))) (cast 32 false (cast 64 false (var g1))))) (cast 64 (msb (cast 32 false (cast 64 false (var g1)))) (cast 32 false (cast 64 false (var g1)))))) (set res128_mid (sdiv (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (|| (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (sle (var res128) (bv 128 0xffffffffffffffffffffffff80000001)))) empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 64 0x7fffffff) (ite (sle (var res128) (bv 128 0xffffffffffffffffffffffff80000001)) (bv 64 0xffffffff80000000) (cast 64 (msb (var res128)) (var res128))))))
dE "mulscc l1, l2, l3" a7244012 0x0 (seq (set rs1 (cast 32 false (cast 64 false (var l1)))) (set arg0 (cast 128 false (ite (lsb (var y)) (cast 32 false (cast 64 false (var l2))) (bv 32 0x0)))) (set arg1 (cast 128 false (>> (var rs1) (bv 8 0x1) (^^ (lsb (>> (var ccr) (bv 8 0x3) false)) (lsb (>> (var ccr) (bv 8 0x1) false)))))) (set res128_mid (+ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (! (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1))))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (! (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1))))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (^^ (^^ (msb (cast 33 false (var arg0))) (msb (cast 33 false (var arg1)))) (msb (cast 33 false (var res128))))) (set carry64 (msb (cast 65 false (var res128)))) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set l3 (cast 64 false (var res128))) (set y (cast 64 false (>> (cast 32 false (var y)) (bv 8 0x1) (lsb (var rs1))))))
dE "mulx l1, l2, l3" a64c4012 0x0 (set l3 (cast 64 false (* (cast 64 false (var l1)) (cast 64 false (var l2)))))
dE "sdivx l1, l2, l3" a76c4012 0x0 (set l3 (cast 64 false (sdiv (cast 64 false (var l1)) (cast 64 false (var l2)))))
dE "udivx l1, l2, l3" a66c4012 0x0 (set l3 (cast 64 false (div (cast 64 false (var l1)) (cast 64 false (var l2)))))
dE "and g1, g2, g3" 86084002 0x0 (set g3 (cast 64 false (& (cast 64 false (var g1)) (cast 64 false (var g2)))))
dE "andn g1, g2, g3" 86284002 0x0 (set g3 (cast 64 false (& (cast 64 false (var g1)) (~ (cast 64 false (var g2))))))
dE "or g1, g2, g3" 86104002 0x0 (set g3 (cast 64 false (| (cast 64 false (var g1)) (cast 64 false (var g2)))))
dE "orn g1, g2, g3" 86304002 0x0 (set g3 (cast 64 false (| (cast 64 false (var g1)) (~ (cast 64 false (var g2))))))
dE "xor g1, g2, g3" 86184002 0x0 (set g3 (cast 64 false (^ (cast 64 false (var g1)) (cast 64 false (var g2)))))
dE "xnor g1, g2, g3" 86384002 0x0 (set g3 (cast 64 false (~ (^ (cast 64 false (var g1)) (cast 64 false (var g2))))))
dE "andcc g2, g1, g3" 86888001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (cast 64 false (var g1)))) (set res128_mid (& (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "andncc g2, g1, g3" 86a88001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (~ (cast 64 false (var g1))))) (set res128_mid (& (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "orcc g2, g1, g3" 86908001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (cast 64 false (var g1)))) (set res128_mid (| (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "orncc g2, g1, g3" 86b08001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (~ (cast 64 false (var g1))))) (set res128_mid (| (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "xorcc g2, g1, g3" 86988001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (cast 64 false (var g1)))) (set res128_mid (^ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "xnorcc g2, g1, g3" 86b88001 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var g2)))) (set arg1 (cast 128 false (~ (cast 64 false (var g1))))) (set res128_mid (^ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) empty empty empty empty (set ccr (| (ite false (bv 8 0x1) (bv 8 0x0)) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set g3 (cast 64 false (var res128))))
dE "jmpl g1+i2, g2" 85c0401a 0x40 (set g2 (bv 64 0x40))
dE "jmpl o1+8, g2" 85c26008 0x40 (set g2 (bv 64 0x40))
dE "jmpl g1, g2" 85c06000 0x40 (set g2 (bv 64 0x40))
dE "call g1+i2" 9fc0401a 0x40 (set o7 (bv 64 0x40))
dE "call o1+8" 9fc26008 0x40 (set o7 (bv 64 0x40))
dE "call g1" 9fc06000 0x40 (set o7 (bv 64 0x40))
dE "call g1;nop;call g1;nop" 9fc06000010000009fc0600001000000 0x40 (set o7 (bv 64 0x40));(seq (set EA (cast 64 false (var g1))) empty (jmp (var EA)));(set o7 (bv 64 0x48));(seq (set EA (cast 64 false (var g1))) empty (jmp (var EA)))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bg 0x1000;nop" 1480040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ble 0x1000;nop" 0480040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bge 0x1000;nop" 1680040001000000 0x0 nop;(branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bl 0x1000;nop" 0680040001000000 0x0 nop;(branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bgu 0x1000;nop" 1880040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bleu 0x1000;nop" 0880040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ba,a xcc, 0x1000;nop" 3068040001000000 0x0 (jmp (cast 64 false (bv 64 0x1000)));nop
dE "bn,a xcc, 0x1000;nop" 2068040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bne,a xcc, 0x1000;nop" 3268040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "be,a xcc, 0x1000;nop" 2268040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bg,a xcc, 0x1000;nop" 3468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "ble,a xcc, 0x1000;nop" 2468040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bge,a xcc, 0x1000;nop" 3668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bl,a xcc, 0x1000;nop" 2668040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bgu,a xcc, 0x1000;nop" 3868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bleu,a xcc, 0x1000;nop" 2868040001000000 0x0 nop;(branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bcc,a xcc, 0x1000;nop" 3a68040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x4) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bcs,a xcc, 0x1000;nop" 2a68040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x4) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bpos,a xcc, 0x1000;nop" 3c68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bneg,a xcc, 0x1000;nop" 2c68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bvc,a xcc, 0x1000;nop" 3e68040001000000 0x0 nop;(branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "bvs,a xcc, 0x1000;nop" 2e68040001000000 0x0 nop;(branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "ldsb [i0+l6], o2" d44e0016 0x0 (set o2 (cast 64 (msb (loadw 0 8 (+ (var i0) (var l6)))) (loadw 0 8 (+ (var i0) (var l6)))))
dE "ldsb [i0+0x20], o2" d44e2020 0x0 (set o2 (cast 64 (msb (loadw 0 8 (+ (var i0) (bv 64 0x20)))) (loadw 0 8 (+ (var i0) (bv 64 0x20)))))
dE "ldsb [g1], o4" d8484000 0x0 (set o4 (cast 64 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))
dE "ldsh [i0+l6], o2" d4560016 0x0 (set o2 (cast 64 (msb (loadw 0 16 (+ (var i0) (var l6)))) (loadw 0 16 (+ (var i0) (var l6)))))
dE "ldsh [i0+0x20], o2" d4562020 0x0 (set o2 (cast 64 (msb (loadw 0 16 (+ (var i0) (bv 64 0x20)))) (loadw 0 16 (+ (var i0) (bv 64 0x20)))))
dE "ldsh [g1], o4" d8504000 0x0 (set o4 (cast 64 (msb (loadw 0 16 (var g1))) (loadw 0 16 (var g1))))
dE "ldub [i0+l6], o2" d40e0016 0x0 (set o2 (cast 64 false (loadw 0 8 (+ (var i0) (var l6)))))
dE "ldub [i0+0x20], o2" d40e2020 0x0 (set o2 (cast 64 false (loadw 0 8 (+ (var i0) (bv 64 0x20)))))
dE "ldub [g1], o2" d4084000 0x0 (set o2 (cast 64 false (loadw 0 8 (var g1))))
dE "lduh [i0+l6], o2" d4160016 0x0 (set o2 (cast 64 false (loadw 0 16 (+ (var i0) (var l6)))))
dE "lduh [i0+0x20], o2" d4162020 0x0 (set o2 (cast 64 false (loadw 0 16 (+ (var i0) (bv 64 0x20)))))
dE "lduh [g1], o2" d4104000 0x0 (set o2 (cast 64 false (loadw 0 16 (var g1))))
dE "ld [i0+l6], o2" d4060016 0x0 (set o2 (cast 64 false (loadw 0 32 (+ (var i0) (var l6)))))
dE "ld [i0+0x20], o2" d4062020 0x0 (set o2 (cast 64 false (loadw 0 32 (+ (var i0) (bv 64 0x20)))))
dE "ld [g1], o2" d4004000 0x0 (set o2 (cast 64 false (loadw 0 32 (var g1))))
dE "ldx [i0+l6], o2" d45e0016 0x0 (set o2 (cast 64 false (loadw 0 64 (+ (var i0) (var l6)))))
dE "ldx [i0+0x20], o2" d45e2020 0x0 (set o2 (cast 64 false (loadw 0 64 (+ (var i0) (bv 64 0x20)))))
dE "ldx [g1], o2" d4584000 0x0 (set o2 (cast 64 false (loadw 0 64 (var g1))))
dE "ldd [i0+l6], o2" d41e0016 0x0 (seq (set load (loadw 0 64 (+ (var i0) (var l6)))) (set o3 (cast 64 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 64 false (>> (var load) (bv 8 0x20) false))))
dE "ldd [i0+0x20], o2" d41e2020 0x0 (seq (set load (loadw 0 64 (+ (var i0) (bv 64 0x20)))) (set o3 (cast 64 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 64 false (>> (var load) (bv 8 0x20) false))))
dE "ldd [g1], o2" d4184000 0x0 (seq (set load (loadw 0 64 (var g1))) (set o3 (cast 64 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 64 false (>> (var load) (bv 8 0x20) false))))
dE "lda [g1] 1, o2" d4804020 0x0 (set o2 (cast 64 false (loadw 0 32 (var g1))))
dE "ldsba [g1] 1, o2" d4c84020 0x0 (set o2 (cast 64 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))
dE "lduba [g1] 1, o2" d4884020 0x0 (set o2 (cast 64 false (loadw 0 8 (var g1))))
dE "ldsha [g1] 1, o2" d4d04020 0x0 (set o2 (cast 64 (msb (loadw 0 16 (var g1))) (loadw 0 16 (var g1))))
dE "lduha [g1] 1, o2" d4904020 0x0 (set o2 (cast 64 false (loadw 0 16 (var g1))))
dE "ldswa [g1] 1, o2" d4c04020 0x0 (set o2 (cast 64 (msb (loadw 0 32 (var g1))) (loadw 0 32 (var g1))))
dE "lda [g1] 1, o2" d4804020 0x0 (set o2 (cast 64 false (loadw 0 32 (var g1))))
dE "ldxa [g1] 1, o2" d4d84020 0x0 (set o2 (cast 64 false (loadw 0 64 (var g1))))
dE "ldda [g1] 1, o2" d4984020 0x0 (seq (set load (loadw 0 64 (var g1))) (set o3 (cast 64 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 64 false (>> (var load) (bv 8 0x20) false))))
dE "ldstuba [i0+l6] 1, o2" d4ee0036 0x0 (seq (set o2 (cast 64 false (loadw 0 8 (+ (var i0) (var l6))))) (storew 0 (+ (var i0) (var l6)) (bv 8 0xff)))
dE "stb o2, [i0+l6]" d42e0016 0x0 (storew 0 (+ (var i0) (var l6)) (cast 8 false (var o2)))
dE "stb o2, [i0+0x20]" d42e2020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (cast 8 false (var o2)))
dE "stb o2, [g1]" d4284000 0x0 (storew 0 (var g1) (cast 8 false (var o2)))
dE "sth o2, [i0+l6]" d4360016 0x0 (storew 0 (+ (var i0) (var l6)) (cast 16 false (var o2)))
dE "sth o2, [i0+0x20]" d4362020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (cast 16 false (var o2)))
dE "sth o2, [g1]" d4304000 0x0 (storew 0 (var g1) (cast 16 false (var o2)))
dE "st o2, [i0+l6]" d4260016 0x0 (storew 0 (+ (var i0) (var l6)) (cast 32 false (var o2)))
dE "st o2, [i0+0x20]" d4262020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (cast 32 false (var o2)))
dE "st o2, [g1]" d4204000 0x0 (storew 0 (var g1) (cast 32 false (var o2)))
dE "stx o2, [i0+l6]" d4760016 0x0 (storew 0 (+ (var i0) (var l6)) (cast 64 false (var o2)))
dE "stx o2, [i0+0x20]" d4762020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (cast 64 false (var o2)))
dE "stx o2, [g1]" d4704000 0x0 (storew 0 (var g1) (cast 64 false (var o2)))
dE "std o2, [i0+l6]" d43e0016 0x0 (storew 0 (+ (var i0) (var l6)) (append (cast 32 false (var o2)) (cast 32 false (var o3))))
dE "std o2, [i0+0x20]" d43e2020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (append (cast 32 false (var o2)) (cast 32 false (var o3))))
dE "std o2, [g1]" d4384000 0x0 (storew 0 (var g1) (append (cast 32 false (var o2)) (cast 32 false (var o3))))
dE "stba o2, [i0+l6] 0x40" d4ae0816 0x0 (storew 0 (+ (var i0) (var l6)) (cast 8 false (var o2)))
dE "stba o2, [g1] 0x40" d4a84800 0x0 (storew 0 (var g1) (cast 8 false (var o2)))
dE "stha o2, [i0+l6] 0x40" d4b60816 0x0 (storew 0 (+ (var i0) (var l6)) (cast 16 false (var o2)))
dE "stha o2, [g1] 0x40" d4b04800 0x0 (storew 0 (var g1) (cast 16 false (var o2)))
dE "sta o2, [i0+l6] 0x40" d4a60816 0x0 (storew 0 (+ (var i0) (var l6)) (cast 32 false (var o2)))
dE "sta o2, [g1] 0x40" d4a04800 0x0 (storew 0 (var g1) (cast 32 false (var o2)))
dE "stxa o2, [i0+l6] 0x40" d4f60816 0x0 (storew 0 (+ (var i0) (var l6)) (cast 64 false (var o2)))
dE "stxa o2, [g1] 0x40" d4f04800 0x0 (storew 0 (var g1) (cast 64 false (var o2)))
dE "stda o2, [i0+l6] 0x40" d4be0816 0x0 (storew 0 (+ (var i0) (var l6)) (append (cast 32 false (var o2)) (cast 32 false (var o3))))
dE "stda o2, [g1] 0x40" d4b84800 0x0 (storew 0 (var g1) (append (cast 32 false (var o2)) (cast 32 false (var o3))))

dE "sll g1, g2, g3" 87284002 0x0 (set g3 (cast 64 false (<< (cast 32 false (cast 64 false (var g1))) (cast 5 false (var g2)) false)))
dE "sll g1, 0x1f, g3" 8728601f 0x0 (set g3 (cast 64 false (<< (cast 32 false (cast 64 false (var g1))) (cast 5 false (bv 64 0x1f)) false)))
dE "srl g1, g2, g3" 87304002 0x0 (set g3 (cast 64 false (>> (cast 32 false (cast 64 false (var g1))) (cast 5 false (var g2)) false)))
dE "srl g1, 0x1f, g3" 8730601f 0x0 (set g3 (cast 64 false (>> (cast 32 false (cast 64 false (var g1))) (cast 5 false (bv 64 0x1f)) false)))
dE "sra g1, g2, g3" 87384002 0x0 (set g3 (cast 64 false (>> (cast 32 false (cast 64 false (var g1))) (cast 5 false (var g2)) (msb (cast 32 false (cast 64 false (var g1)))))))
dE "sra g1, 0x1f, g3" 8738601f 0x0 (set g3 (cast 64 false (>> (cast 32 false (cast 64 false (var g1))) (cast 5 false (bv 64 0x1f)) (msb (cast 32 false (cast 64 false (var g1)))))))

dE "sethi 0x16, g1" 03000016 0x0 (set g1 (cast 64 false (<< (bv 64 0x16) (bv 8 0xa) false)))

dE "mov g1, g3" 86100001 0x0 (set g3 (cast 64 false (| (cast 64 false (var g0)) (cast 64 false (var g1)))))
dE "mov 0xff, g3" 861020ff 0x0 (set g3 (cast 64 false (| (cast 64 false (var g0)) (cast 64 false (bv 64 0xff)))))

dE "te xcc, 0x10" 83d03010 0x0 (branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false)) (goto trap) nop)
dE "tle icc, i3" 85d0001b 0x0 (branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (goto trap) nop)

dE "save o0, l1, i7" bfe20011 0x0 (seq (set add_result (+ (cast 64 false (var o0)) (cast 64 false (var l1)))) (set reg_window_base (* (var cwp) (bv 64 0x400))) (storew 1 (+ (var reg_window_base) (bv 64 0x0)) (var l0)) (storew 1 (+ (var reg_window_base) (bv 64 0x40)) (var l1)) (storew 1 (+ (var reg_window_base) (bv 64 0x80)) (var l2)) (storew 1 (+ (var reg_window_base) (bv 64 0xc0)) (var l3)) (storew 1 (+ (var reg_window_base) (bv 64 0x100)) (var l4)) (storew 1 (+ (var reg_window_base) (bv 64 0x140)) (var l5)) (storew 1 (+ (var reg_window_base) (bv 64 0x180)) (var l6)) (storew 1 (+ (var reg_window_base) (bv 64 0x1c0)) (var l7)) (storew 1 (+ (var reg_window_base) (bv 64 0x200)) (var i0)) (storew 1 (+ (var reg_window_base) (bv 64 0x240)) (var i1)) (storew 1 (+ (var reg_window_base) (bv 64 0x280)) (var i2)) (storew 1 (+ (var reg_window_base) (bv 64 0x2c0)) (var i3)) (storew 1 (+ (var reg_window_base) (bv 64 0x300)) (var i4)) (storew 1 (+ (var reg_window_base) (bv 64 0x340)) (var i5)) (storew 1 (+ (var reg_window_base) (bv 64 0x380)) (var fp)) (storew 1 (+ (var reg_window_base) (bv 64 0x3c0)) (var i7)) (set cwp (mod (+ (var cwp) (bv 64 0x1)) (bv 64 0x8))) (set i0 (var o0)) (set i1 (var o1)) (set i2 (var o2)) (set i3 (var o3)) (set i4 (var o4)) (set i5 (var o5)) (set fp (var sp)) (set i7 (var o7)) (set l0 (bv 64 0x0)) (set l1 (bv 64 0x0)) (set l2 (bv 64 0x0)) (set l3 (bv 64 0x0)) (set l4 (bv 64 0x0)) (set l5 (bv 64 0x0)) (set l6 (bv 64 0x0)) (set l7 (bv 64 0x0)) (set o0 (bv 64 0x0)) (set o1 (bv 64 0x0)) (set o2 (bv 64 0x0)) (set o3 (bv 64 0x0)) (set o4 (bv 64 0x0)) (set o5 (bv 64 0x0)) (set sp (bv 64 0x0)) (set o7 (bv 64 0x0)) (set i7 (var add_result)))
dE "restore o0, l1, i7" bfea0011 0x0 (seq (set add_result (+ (cast 64 false (var o0)) (cast 64 false (var l1)))) (set cwp (mod (- (var cwp) (bv 64 0x1)) (bv 64 0x8))) (set o0 (var i0)) (set o1 (var i1)) (set o2 (var i2)) (set o3 (var i3)) (set o4 (var i4)) (set o5 (var i5)) (set sp (var fp)) (set o7 (var i7)) (set reg_window_base (* (var cwp) (bv 64 0x400))) (set l0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x0)))) (set l1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x40)))) (set l2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x80)))) (set l3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0xc0)))) (set l4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x100)))) (set l5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x140)))) (set l6 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x180)))) (set l7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x1c0)))) (set i0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x200)))) (set i1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x240)))) (set i2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x280)))) (set i3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x2c0)))) (set i4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x300)))) (set i5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x340)))) (set fp (loadw 1 64 (+ (var reg_window_base) (bv 64 0x380)))) (set i7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x3c0)))) (set i7 (var add_result)))

dE "brz i0, 0x1000;nop" 02ce040001000000 0x0 nop;(branch (is_zero (var i0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brlez i0, 0x1000;nop" 04ce040001000000 0x0 nop;(branch (sle (var i0) (bv 64 0x0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brlz i0, 0x1000;nop" 06ce040001000000 0x0 nop;(branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brnz i0, 0x1000;nop" 0ace040001000000 0x0 nop;(branch (! (is_zero (var i0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brgz i0, 0x1000;nop" 0cce040001000000 0x0 nop;(branch (! (sle (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "brgez i0, 0x1000;nop" 0ece040001000000 0x0 nop;(branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))

dE "brz,a i0, 0x1000;nop" 22ce040001000000 0x0 nop;(branch (is_zero (var i0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brlez,a i0, 0x1000;nop" 24ce040001000000 0x0 nop;(branch (sle (var i0) (bv 64 0x0)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brlz,a i0, 0x1000;nop" 26ce040001000000 0x0 nop;(branch (&& (sle (var i0) (bv 64 0x0)) (! (== (var i0) (bv 64 0x0)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brnz,a i0, 0x1000;nop" 2ace040001000000 0x0 nop;(branch (! (is_zero (var i0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brgz,a i0, 0x1000;nop" 2cce040001000000 0x0 nop;(branch (! (sle (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "brgez,a i0, 0x1000;nop" 2ece040001000000 0x0 nop;(branch (|| (! (sle (var i0) (bv 64 0x0))) (== (var i0) (bv 64 0x0))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))

dE "wr i0, g1, y" 81860001 0x0 (set y (^ (var i0) (var g1)))
dE "wr i0, g1, ccr" 85860001 0x0 (set ccr (cast 8 false (^ (var i0) (var g1))))
dE "wr i0, g1, asi" 87860001 0x0 (set asi (^ (var i0) (var g1)))
dE "wr i0, g1, fprs" 8d860001 0x0 (set fprs (cast 3 false (^ (var i0) (var g1))))
dE "wr i0, g1, asr19" a7860001 0x0 (set gsr (^ (var i0) (var g1)))
dE "wr i0, g1, asr22" ad860001 0x0 (set asr22 (^ (var i0) (var g1)))
dE "wr i0, g1, asr25" b3860001 0x0 (set asr25 (^ (var i0) (var g1)))

dE "wr i0, 0x100, y" 81862100 0x0 (set y (^ (var i0) (bv 64 0x100)))
dE "wr i0, 0x100, ccr" 85862100 0x0 (set ccr (cast 8 false (^ (var i0) (bv 64 0x100))))
dE "wr i0, 0x100, asi" 87862100 0x0 (set asi (^ (var i0) (bv 64 0x100)))
dE "wr i0, 0x100, fprs" 8d862100 0x0 (set fprs (cast 3 false (^ (var i0) (bv 64 0x100))))
dE "wr i0, 0x100, asr19" a7862100 0x0 (set gsr (^ (var i0) (bv 64 0x100)))
dE "wr i0, 0x100, asr22" ad862100 0x0 (set asr22 (^ (var i0) (bv 64 0x100)))
dE "wr i0, 0x100, asr25" b3862100 0x0 (set asr25 (^ (var i0) (bv 64 0x100)))

dE "rd y, i0" b1400000 0x0 (set i0 (var y))
dE "rd ccr, i0" b1408000 0x0 (set i0 (cast 64 false (var ccr)))
dE "rd asi, i0" b140c000 0x0 (set i0 (var asi))
dE "rd fprs, i0" b1418000 0x0 (set i0 (cast 64 false (var fprs)))
dE "rd asr19, i0" b144c000 0x0 (set i0 (var asr19))
dE "rd asr22, i0" b1458000 0x0 (set i0 (var asr22))
dE "rd asr25, i0" b1464000 0x0 (set i0 (var asr25))

dE "rett i7+8" 81cfe008 0x0 (seq (set tnpc (cast 64 false (+ (var i7) (bv 64 0x8)))) empty (set cwp (mod (- (var cwp) (bv 64 0x1)) (bv 64 0x8))) (set o0 (var i0)) (set o1 (var i1)) (set o2 (var i2)) (set o3 (var i3)) (set o4 (var i4)) (set o5 (var i5)) (set sp (var fp)) (set o7 (var i7)) (set reg_window_base (* (var cwp) (bv 64 0x400))) (set l0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x0)))) (set l1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x40)))) (set l2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x80)))) (set l3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0xc0)))) (set l4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x100)))) (set l5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x140)))) (set l6 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x180)))) (set l7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x1c0)))) (set i0 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x200)))) (set i1 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x240)))) (set i2 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x280)))) (set i3 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x2c0)))) (set i4 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x300)))) (set i5 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x340)))) (set fp (loadw 1 64 (+ (var reg_window_base) (bv 64 0x380)))) (set i7 (loadw 1 64 (+ (var reg_window_base) (bv 64 0x3c0)))) empty)

# VIS only

dE "cmask8 i7" 81b0037f 0x0 (seq (set rs2 (var i7)) (set mask (bv 32 0x0)) (set mask (| (var mask) (<< (ite (msb (cast 1 false (var rs2))) (bv 32 0x7) (bv 32 0xf)) (bv 8 0x0) false))) (set mask (| (var mask) (<< (ite (msb (cast 2 false (var rs2))) (bv 32 0x6) (bv 32 0xe)) (bv 8 0x4) false))) (set mask (| (var mask) (<< (ite (msb (cast 3 false (var rs2))) (bv 32 0x5) (bv 32 0xd)) (bv 8 0x8) false))) (set mask (| (var mask) (<< (ite (msb (cast 4 false (var rs2))) (bv 32 0x4) (bv 32 0xc)) (bv 8 0xc) false))) (set mask (| (var mask) (<< (ite (msb (cast 5 false (var rs2))) (bv 32 0x3) (bv 32 0xb)) (bv 8 0x10) false))) (set mask (| (var mask) (<< (ite (msb (cast 6 false (var rs2))) (bv 32 0x2) (bv 32 0xa)) (bv 8 0x14) false))) (set mask (| (var mask) (<< (ite (msb (cast 7 false (var rs2))) (bv 32 0x1) (bv 32 0x9)) (bv 8 0x18) false))) (set mask (| (var mask) (<< (ite (msb (cast 8 false (var rs2))) (bv 32 0x0) (bv 32 0x8)) (bv 8 0x1c) false))) (set gsr (& (var gsr) (bv 64 0xffffffff))) (set gsr (| (var gsr) (append (var mask) (bv 32 0x0)))))
dE "cmask16 i7" 81b003bf 0x0 (seq (set rs2 (var i7)) (set mask (bv 32 0x0)) (set mask (| (var mask) (<< (ite (msb (cast 1 false (var rs2))) (bv 32 0x67) (bv 32 0xef)) (bv 8 0x0) false))) (set mask (| (var mask) (<< (ite (msb (cast 2 false (var rs2))) (bv 32 0x45) (bv 32 0xcd)) (bv 8 0x8) false))) (set mask (| (var mask) (<< (ite (msb (cast 3 false (var rs2))) (bv 32 0x23) (bv 32 0xab)) (bv 8 0x10) false))) (set mask (| (var mask) (<< (ite (msb (cast 4 false (var rs2))) (bv 32 0x1) (bv 32 0x89)) (bv 8 0x18) false))) (set gsr (& (var gsr) (bv 64 0xffffffff))) (set gsr (| (var gsr) (append (var mask) (bv 32 0x0)))))
dE "cmask32 i7" 81b003ff 0x0 (seq (set rs2 (var i7)) (set mask (bv 32 0x0)) (set mask (| (var mask) (<< (ite (msb (cast 1 false (var rs2))) (bv 32 0x4567) (bv 32 0xcdef)) (bv 8 0x0) false))) (set mask (| (var mask) (<< (ite (msb (cast 2 false (var rs2))) (bv 32 0x123) (bv 32 0x89ab)) (bv 8 0x10) false))) (set gsr (& (var gsr) (bv 64 0xffffffff))) (set gsr (| (var gsr) (append (var mask) (bv 32 0x0)))))

dE "edge16 i0, i1, g1" 83b60099 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x6) (var rs1)) (bv 8 0x1) false)) (set lmask (cast 64 false (>> (bv 4 0xf) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x6) (var rs2)) (bv 8 0x1) false)) (set rmask (cast 64 false (>> (bv 4 0x8) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge16l i0, i1, g1" 83b600d9 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x6) (var rs1)) (bv 8 0x1) false)) (set lmask (cast 64 false (<< (bv 4 0xf) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x6) (var rs2)) (bv 8 0x1) false)) (set rmask (cast 64 false (<< (bv 4 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge16ln i0, i1, g1" 83b600f9 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x6) (var rs1)) (bv 8 0x1) false)) (set lmask (cast 64 false (<< (bv 4 0xf) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x6) (var rs2)) (bv 8 0x1) false)) (set rmask (cast 64 false (<< (bv 4 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))
dE "edge16n i0, i1, g1" 83b600b9 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x6) (var rs1)) (bv 8 0x1) false)) (set lmask (cast 64 false (>> (bv 4 0xf) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x6) (var rs2)) (bv 8 0x1) false)) (set rmask (cast 64 false (>> (bv 4 0x8) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))
dE "edge32 i0, i1, g1" 83b60119 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x4) (var rs1)) (bv 8 0x2) false)) (set lmask (cast 64 false (>> (bv 2 0x3) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x4) (var rs2)) (bv 8 0x2) false)) (set rmask (cast 64 false (>> (bv 2 0x2) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge32l i0, i1, g1" 83b60159 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x4) (var rs1)) (bv 8 0x2) false)) (set lmask (cast 64 false (<< (bv 2 0x3) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x4) (var rs2)) (bv 8 0x2) false)) (set rmask (cast 64 false (<< (bv 2 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge32ln i0, i1, g1" 83b60179 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x4) (var rs1)) (bv 8 0x2) false)) (set lmask (cast 64 false (<< (bv 2 0x3) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x4) (var rs2)) (bv 8 0x2) false)) (set rmask (cast 64 false (<< (bv 2 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))
dE "edge32n i0, i1, g1" 83b60139 0x0 (seq (set rs1 (var i0)) (set shft_amt (>> (& (bv 64 0x4) (var rs1)) (bv 8 0x2) false)) (set lmask (cast 64 false (>> (bv 2 0x3) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (>> (& (bv 64 0x4) (var rs2)) (bv 8 0x2) false)) (set rmask (cast 64 false (>> (bv 2 0x2) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))
dE "edge8 i0, i1, g1" 83b60019 0x0 (seq (set rs1 (var i0)) (set shft_amt (& (bv 64 0x7) (var rs1))) (set lmask (cast 64 false (>> (bv 8 0xff) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (& (bv 64 0x7) (var rs2))) (set rmask (cast 64 false (>> (bv 8 0x80) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge8l i0, i1, g1" 83b60059 0x0 (seq (set rs1 (var i0)) (set shft_amt (& (bv 64 0x7) (var rs1))) (set lmask (cast 64 false (<< (bv 8 0xff) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (& (bv 64 0x7) (var rs2))) (set rmask (cast 64 false (<< (bv 8 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))) (set arg0 (cast 128 false (var rs1))) (set arg1 (cast 128 false (var rs2))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))))
dE "edge8ln i0, i1, g1" 83b60079 0x0 (seq (set rs1 (var i0)) (set shft_amt (& (bv 64 0x7) (var rs1))) (set lmask (cast 64 false (<< (bv 8 0xff) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (& (bv 64 0x7) (var rs2))) (set rmask (cast 64 false (<< (bv 8 0x1) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))
dE "edge8n i0, i1, g1" 83b60039 0x0 (seq (set rs1 (var i0)) (set shft_amt (& (bv 64 0x7) (var rs1))) (set lmask (cast 64 false (>> (bv 8 0xff) (var shft_amt) false))) (set rs2 (var i1)) (set shft_amt (& (bv 64 0x7) (var rs2))) (set rmask (cast 64 false (>> (bv 8 0x80) (var shft_amt) true))) (branch (== (>> (var rs1) (bv 8 0x3) false) (>> (var rs2) (bv 8 0x3) false)) (set g1 (& (var rmask) (var lmask))) (set g1 (var lmask))))

dE "flcmpd fcc2, f0, f4" 85b02a44 0x0 (seq (set flx (float 4 (var f0) )) (set fly (float 4 (var f4) )) (set fcc_v (ite (is_nan (var fly)) (bv 64 0x3) (ite (is_nan (var flx)) (bv 64 0x2) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x0))))) (set sh (bv 8 0x22)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))
dE "flcmps fcc3, f0, f4" 87b02a24 0x0 (seq (set flx (float 4 (var f0) )) (set fly (float 4 (var f4) )) (set fcc_v (ite (is_nan (var fly)) (bv 64 0x3) (ite (is_nan (var flx)) (bv 64 0x2) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x0))))) (set sh (bv 8 0x24)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))

dE "fsrc1 f0, f4" 89b00e80 0x0 (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsrc2 f0, f4" 89b00f00 0x0 (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsrc1s f0, f4" 89b00ea0 0x0 (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsrc2s f0, f4" 89b00f20 0x0 (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fslas16 f0, f2, f4" 89b00522 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 16 0x8000)) (set sat_max (bv 16 0x7fff)) (set part (cast 16 false (>> (var rs1) (bv 8 0x0) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 4 false (>> (var rs2) (bv 8 0x0) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x0) false))) (set part (cast 16 false (>> (var rs1) (bv 8 0x10) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 4 false (>> (var rs2) (bv 8 0x10) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x10) false))) (set part (cast 16 false (>> (var rs1) (bv 8 0x20) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 4 false (>> (var rs2) (bv 8 0x20) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x20) false))) (set part (cast 16 false (>> (var rs1) (bv 8 0x30) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 4 false (>> (var rs2) (bv 8 0x30) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x30) false))))
dE "fslas32 f0, f2, f4" 89b005a2 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 32 0x80000000)) (set sat_max (bv 32 0x7fffffff)) (set part (cast 32 false (>> (var rs1) (bv 8 0x0) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 5 false (>> (var rs2) (bv 8 0x0) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x0) false))) (set part (cast 32 false (>> (var rs1) (bv 8 0x20) false))) (set orig_sign (msb (var part))) (set shft_res (<< (var part) (cast 5 false (>> (var rs2) (bv 8 0x20) false)) false)) (set new_part (ite (! (^^ (var orig_sign) (msb (var shft_res)))) (var part) (ite (var orig_sign) (var sat_min) (var sat_max)))) (set res (| (var res) (<< (cast 64 false (var new_part)) (bv 8 0x20) false))))
dE "fsll16 f0, f2, f4" 89b00422 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 16 0x8000)) (set sat_max (bv 16 0x7fff)) (set res (| (var res) (<< (cast 64 false (<< (cast 16 false (>> (var rs1) (bv 8 0x0) false)) (cast 4 false (>> (var rs2) (bv 8 0x0) false)) false)) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (<< (cast 16 false (>> (var rs1) (bv 8 0x10) false)) (cast 4 false (>> (var rs2) (bv 8 0x10) false)) false)) (bv 8 0x10) false))) (set res (| (var res) (<< (cast 64 false (<< (cast 16 false (>> (var rs1) (bv 8 0x20) false)) (cast 4 false (>> (var rs2) (bv 8 0x20) false)) false)) (bv 8 0x20) false))) (set res (| (var res) (<< (cast 64 false (<< (cast 16 false (>> (var rs1) (bv 8 0x30) false)) (cast 4 false (>> (var rs2) (bv 8 0x30) false)) false)) (bv 8 0x30) false))))
dE "fsll32 f0, f2, f4" 89b004a2 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 32 0x80000000)) (set sat_max (bv 32 0x7fffffff)) (set res (| (var res) (<< (cast 64 false (<< (cast 32 false (>> (var rs1) (bv 8 0x0) false)) (cast 5 false (>> (var rs2) (bv 8 0x0) false)) false)) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (<< (cast 32 false (>> (var rs1) (bv 8 0x20) false)) (cast 5 false (>> (var rs2) (bv 8 0x20) false)) false)) (bv 8 0x20) false))))
dE "fsra16 f0, f2, f4" 89b00562 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 16 0x8000)) (set sat_max (bv 16 0x7fff)) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x0) false)) (cast 4 false (>> (var rs2) (bv 8 0x0) false)) (msb (cast 16 false (>> (var rs1) (bv 8 0x0) false))))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x10) false)) (cast 4 false (>> (var rs2) (bv 8 0x10) false)) (msb (cast 16 false (>> (var rs1) (bv 8 0x10) false))))) (bv 8 0x10) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x20) false)) (cast 4 false (>> (var rs2) (bv 8 0x20) false)) (msb (cast 16 false (>> (var rs1) (bv 8 0x20) false))))) (bv 8 0x20) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x30) false)) (cast 4 false (>> (var rs2) (bv 8 0x30) false)) (msb (cast 16 false (>> (var rs1) (bv 8 0x30) false))))) (bv 8 0x30) false))))
dE "fsra32 f0, f2, f4" 89b005e2 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 32 0x80000000)) (set sat_max (bv 32 0x7fffffff)) (set res (| (var res) (<< (cast 64 false (>> (cast 32 false (>> (var rs1) (bv 8 0x0) false)) (cast 5 false (>> (var rs2) (bv 8 0x0) false)) (msb (cast 32 false (>> (var rs1) (bv 8 0x0) false))))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 32 false (>> (var rs1) (bv 8 0x20) false)) (cast 5 false (>> (var rs2) (bv 8 0x20) false)) (msb (cast 32 false (>> (var rs1) (bv 8 0x20) false))))) (bv 8 0x20) false))))
dE "fsrl16 f0, f2, f4" 89b00462 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 16 0x8000)) (set sat_max (bv 16 0x7fff)) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x0) false)) (cast 4 false (>> (var rs2) (bv 8 0x0) false)) false)) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x10) false)) (cast 4 false (>> (var rs2) (bv 8 0x10) false)) false)) (bv 8 0x10) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x20) false)) (cast 4 false (>> (var rs2) (bv 8 0x20) false)) false)) (bv 8 0x20) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 16 false (>> (var rs1) (bv 8 0x30) false)) (cast 4 false (>> (var rs2) (bv 8 0x30) false)) false)) (bv 8 0x30) false))))
dE "fsrl32 f0, f2, f4" 89b004e2 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (set sat_min (bv 32 0x80000000)) (set sat_max (bv 32 0x7fffffff)) (set res (| (var res) (<< (cast 64 false (>> (cast 32 false (>> (var rs1) (bv 8 0x0) false)) (cast 5 false (>> (var rs2) (bv 8 0x0) false)) false)) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (>> (cast 32 false (>> (var rs1) (bv 8 0x20) false)) (cast 5 false (>> (var rs2) (bv 8 0x20) false)) false)) (bv 8 0x20) false))))

# UltraSparc only

dE "fsqrts f0, f4" 89a00520 0x0 (seq (set bv (fbits (fsqrt rna (float 0 (var f0) )))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsqrtd f0, f4" 89a00540 0x0 (seq (set bv (fbits (fsqrt rna (float 1 (append (var f0) (var f1)) )))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsqrtq f0, f4" 89a00560 0x0 (seq (set bv (fbits (fsqrt rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) )))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fcmps f0, f4" 81a80a24 0x0 (seq (set flx (float 0 (var f0) )) (set fly (float 0 (var f4) )) (set fcc_v (ite (|| (is_nan (var flx)) (is_nan (var fly))) (bv 64 0x3) (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2))))) (set sh (bv 8 0xa)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))
dE "fcmpd fcc1, f0, f4" 83a80a44 0x0 (seq (set flx (float 1 (append (var f0) (var f1)) )) (set fly (float 1 (append (var f4) (var f5)) )) (set fcc_v (ite (|| (is_nan (var flx)) (is_nan (var fly))) (bv 64 0x3) (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2))))) (set sh (bv 8 0x20)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))
dE "fcmpq fcc2, f0, f4" 85a80a64 0x0 (seq (set flx (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) )) (set fly (float 3 (append (append (append (var f4) (var f5)) (var f6)) (var f7)) )) (set fcc_v (ite (|| (is_nan (var flx)) (is_nan (var fly))) (bv 64 0x3) (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2))))) (set sh (bv 8 0x22)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))
dE "fcmpes fcc3, f0, f4" 87a80aa4 0x0 (seq (set flx (float 0 (var f0) )) (set fly (float 0 (var f4) )) (branch (|| (is_nan (var flx)) (is_nan (var fly))) (seq (set sh (bv 8 0x24)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (bv 64 0x3) (var sh) false))) (goto fp_exception)) (seq (set fcc_v (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2)))) (set sh (bv 8 0x24)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))))
dE "fcmped f0, f4" 81a80ac4 0x0 (seq (set flx (float 1 (append (var f0) (var f1)) )) (set fly (float 1 (append (var f4) (var f5)) )) (branch (|| (is_nan (var flx)) (is_nan (var fly))) (seq (set sh (bv 8 0xa)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (bv 64 0x3) (var sh) false))) (goto fp_exception)) (seq (set fcc_v (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2)))) (set sh (bv 8 0xa)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))))
dE "fcmpeq fcc1, f0, f4" 83a80ae4 0x0 (seq (set flx (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) )) (set fly (float 3 (append (append (append (var f4) (var f5)) (var f6)) (var f7)) )) (branch (|| (is_nan (var flx)) (is_nan (var fly))) (seq (set sh (bv 8 0x20)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (bv 64 0x3) (var sh) false))) (goto fp_exception)) (seq (set fcc_v (ite (! (|| (|| (is_nan (var flx)) (is_nan (var fly))) (|| (<. (var flx) (var fly)) (<. (var fly) (var flx))))) (bv 64 0x0) (ite (&& (! (|| (is_nan (var flx)) (is_nan (var fly)))) (<. (var flx) (var fly))) (bv 64 0x1) (bv 64 0x2)))) (set sh (bv 8 0x20)) (set fsr (| (& (var fsr) (~ (<< (bv 64 0x3) (var sh) false))) (<< (var fcc_v) (var sh) false))))))

dE "fcmpeq16 f0, f4, i0" b1b00544 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (== (cast 16 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 16 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (== (cast 16 (msb (>> (var left) (bv 8 0x10) false)) (>> (var left) (bv 8 0x10) false)) (cast 16 (msb (>> (var right) (bv 8 0x10) false)) (>> (var right) (bv 8 0x10) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty) (branch (== (cast 16 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 16 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x2) false))) empty) (branch (== (cast 16 (msb (>> (var left) (bv 8 0x30) false)) (>> (var left) (bv 8 0x30) false)) (cast 16 (msb (>> (var right) (bv 8 0x30) false)) (>> (var right) (bv 8 0x30) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x3) false))) empty))
dE "fcmpeq32 f0, f4, i0" b1b005c4 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (== (cast 32 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 32 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (== (cast 32 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 32 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty))
dE "fcmpgt16 f0, f4, i0" b1b00504 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (! (sle (cast 16 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 16 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (! (sle (cast 16 (msb (>> (var left) (bv 8 0x10) false)) (>> (var left) (bv 8 0x10) false)) (cast 16 (msb (>> (var right) (bv 8 0x10) false)) (>> (var right) (bv 8 0x10) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty) (branch (! (sle (cast 16 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 16 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x2) false))) empty) (branch (! (sle (cast 16 (msb (>> (var left) (bv 8 0x30) false)) (>> (var left) (bv 8 0x30) false)) (cast 16 (msb (>> (var right) (bv 8 0x30) false)) (>> (var right) (bv 8 0x30) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x3) false))) empty))
dE "fcmpgt32 f0, f4, i0" b1b00584 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (! (sle (cast 32 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 32 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (! (sle (cast 32 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 32 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty))
dE "fcmple16 f0, f4, i0" b1b00404 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (sle (cast 16 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 16 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (sle (cast 16 (msb (>> (var left) (bv 8 0x10) false)) (>> (var left) (bv 8 0x10) false)) (cast 16 (msb (>> (var right) (bv 8 0x10) false)) (>> (var right) (bv 8 0x10) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty) (branch (sle (cast 16 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 16 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x2) false))) empty) (branch (sle (cast 16 (msb (>> (var left) (bv 8 0x30) false)) (>> (var left) (bv 8 0x30) false)) (cast 16 (msb (>> (var right) (bv 8 0x30) false)) (>> (var right) (bv 8 0x30) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x3) false))) empty))
dE "fcmple32 f0, f4, i0" b1b00484 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (sle (cast 32 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 32 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (sle (cast 32 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 32 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty))
dE "fcmpne16 f0, f4, i0" b1b00444 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (! (== (cast 16 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 16 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (! (== (cast 16 (msb (>> (var left) (bv 8 0x10) false)) (>> (var left) (bv 8 0x10) false)) (cast 16 (msb (>> (var right) (bv 8 0x10) false)) (>> (var right) (bv 8 0x10) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty) (branch (! (== (cast 16 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 16 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x2) false))) empty) (branch (! (== (cast 16 (msb (>> (var left) (bv 8 0x30) false)) (>> (var left) (bv 8 0x30) false)) (cast 16 (msb (>> (var right) (bv 8 0x30) false)) (>> (var right) (bv 8 0x30) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x3) false))) empty))
dE "fcmpne32 f0, f4, i0" b1b004c4 0x0 (seq (set i0 (bv 64 0x0)) (set left (fbits (float 1 (append (var f0) (var f1)) ))) (set right (fbits (float 1 (append (var f4) (var f5)) ))) (branch (! (== (cast 32 (msb (>> (var left) (bv 8 0x0) false)) (>> (var left) (bv 8 0x0) false)) (cast 32 (msb (>> (var right) (bv 8 0x0) false)) (>> (var right) (bv 8 0x0) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x0) false))) empty) (branch (! (== (cast 32 (msb (>> (var left) (bv 8 0x20) false)) (>> (var left) (bv 8 0x20) false)) (cast 32 (msb (>> (var right) (bv 8 0x20) false)) (>> (var right) (bv 8 0x20) false)))) (set i0 (| (var i0) (<< (bv 64 0x1) (bv 8 0x1) false))) empty))

dE "fdtoi f0, f4" 89a01a40 0x0 (seq (set bv (fcast_int 32 rna (float 1 (append (var f0) (var f1)) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fqtoi f0, f4" 89a01a60 0x0 (seq (set bv (fcast_int 32 rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fstoi f0, f4" 89a01a20 0x0 (seq (set bv (fcast_int 32 rna (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fdtox f0, f4" 89a01040 0x0 (seq (set bv (fcast_int 64 rna (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fqtox f0, f4" 89a01060 0x0 (seq (set bv (fcast_int 64 rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fstox f0, f4" 89a01020 0x0 (seq (set bv (fcast_int 64 rna (float 0 (var f0) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fitos f0, f4" 89a01880 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin32 rna (var f0)))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fxtos f0, f4" 89a01080 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin32 rna (var f0)))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fitod f0, f4" 89a01900 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin64 rna (var f0)))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fxtod f0, f4" 89a01100 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin64 rna (var f0)))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fitoq f0, f4" 89a01980 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin128 rna (var f0)))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fxtoq f0, f4" 89a01180 0x0 (seq (set bv (fbits (fcast_sfloat ieee754-bin128 rna (var f0)))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fdtos f0, f4" 89a018c0 0x0 (seq (set bv (fbits (fconvert ieee754-bin32 rna (float 1 (append (var f0) (var f1)) )))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fqtos f0, f4" 89a018e0 0x0 (seq (set bv (fbits (fconvert ieee754-bin32 rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) )))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fqtod f0, f4" 89a01960 0x0 (seq (set bv (fbits (fconvert ieee754-bin64 rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) )))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fstod f0, f4" 89a01920 0x0 (seq (set bv (fbits (fconvert ieee754-bin64 rna (float 0 (var f0) )))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fdtoq f0, f4" 89a019c0 0x0 (seq (set bv (fbits (fconvert ieee754-bin128 rna (float 1 (append (var f0) (var f1)) )))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fstoq f0, f4" 89a019a0 0x0 (seq (set bv (fbits (fconvert ieee754-bin128 rna (float 0 (var f0) )))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fnegs f0, f0" 81a000a0 0x0 (seq (set bv (fbits (fneg (float 0 (var f0) )))) (set f0 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnegd f32, f0" 81a000c1 0x0 (seq (set bv (fbits (fneg (float 1 (var f32) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnegq f60, f0" 81a000fd 0x0 (seq (set bv (fbits (fneg (float 3 (append (var f60) (var f62)) )))) (set f3 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f2 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f1 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fabss f0, f0" 81a00120 0x0 (seq (set bv (fbits (fabs (float 0 (var f0) )))) (set f0 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fabsd f32, f0" 81a00141 0x0 (seq (set bv (fbits (fabs (float 1 (var f32) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fabsq f60, f0" 81a0017d 0x0 (seq (set bv (fbits (fabs (float 3 (append (var f60) (var f62)) )))) (set f3 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f2 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f1 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fone f32" 83b00fc0 0x0 (seq (set bv (bv 64 0xffffffffffffffff)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fones f0" 81b00fe0 0x0 (seq (set bv (bv 32 0xffffffff)) (set f0 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fzero f32" 83b00c00 0x0 (seq (set bv (bv 64 0x0)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fzeros f0" 81b00c20 0x0 (seq (set bv (bv 32 0x0)) (set f0 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fnot1 f0, f60" bbb00d40 0x0 (seq (set bv (~ (fbits (float 1 (append (var f0) (var f1)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fnot2 f0, f60" bbb00cc0 0x0 (seq (set bv (~ (fbits (float 1 (append (var f0) (var f1)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fnot1s f0, f1" 83b00d60 0x0 (seq (set bv (~ (fbits (float 0 (var f0) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnot2s f0, f1" 83b00ce0 0x0 (seq (set bv (~ (fbits (float 0 (var f0) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fnand f0, f32, f60" bbb00dc1 0x0 (seq (set bv (~ (& (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) ))))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fnor f0, f32, f60" bbb00c41 0x0 (seq (set bv (~ (| (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) ))))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fand f0, f32, f60" bbb00e01 0x0 (seq (set bv (& (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fandnot1 f0, f32, f60" bbb00d01 0x0 (seq (set bv (& (~ (fbits (float 1 (append (var f0) (var f1)) ))) (fbits (float 1 (var f32) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fandnot2 f0, f32, f60" bbb00c81 0x0 (seq (set bv (& (fbits (float 1 (append (var f0) (var f1)) )) (~ (fbits (float 1 (var f32) ))))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fxnor f0, f32, f60" bbb00e41 0x0 (seq (set bv (~ (^ (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) ))))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fxor f0, f32, f60" bbb00d81 0x0 (seq (set bv (^ (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "for f0, f32, f60" bbb00f81 0x0 (seq (set bv (| (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fornot1 f0, f32, f60" bbb00f41 0x0 (seq (set bv (| (~ (fbits (float 1 (append (var f0) (var f1)) ))) (fbits (float 1 (var f32) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fornot2 f0, f32, f60" bbb00ec1 0x0 (seq (set bv (| (fbits (float 1 (append (var f0) (var f1)) )) (~ (fbits (float 1 (var f32) ))))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fnands f0, f16, f30" bdb00df0 0x0 (seq (set bv (~ (& (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) ))))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnors f0, f16, f30" bdb00c70 0x0 (seq (set bv (~ (| (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) ))))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fandnot1s f0, f16, f30" bdb00d30 0x0 (seq (set bv (& (~ (fbits (float 0 (var f0) ))) (fbits (float 0 (var f16) )))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fandnot2s f0, f16, f30" bdb00cb0 0x0 (seq (set bv (& (fbits (float 0 (var f0) )) (~ (fbits (float 0 (var f16) ))))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fands f0, f16, f30" bdb00e30 0x0 (seq (set bv (& (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) )))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fxnors f0, f16, f30" bdb00e70 0x0 (seq (set bv (~ (^ (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) ))))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fxors f0, f16, f30" bdb00db0 0x0 (seq (set bv (^ (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) )))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fornot1s f0, f16, f30" bdb00f70 0x0 (seq (set bv (| (~ (fbits (float 0 (var f0) ))) (fbits (float 0 (var f16) )))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fornot2s f0, f16, f30" bdb00ef0 0x0 (seq (set bv (| (fbits (float 0 (var f0) )) (~ (fbits (float 0 (var f16) ))))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fors f0, f16, f30" bdb00fb0 0x0 (seq (set bv (| (fbits (float 0 (var f0) )) (fbits (float 0 (var f16) )))) (set f30 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

# V9 only

dE "fba 0x4000;nop" 1180100001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbn 0x4000;nop" 0180100001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbu 0x4000;nop" 0f80100001000000 0x0 nop;(branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbg 0x4000;nop" 0d80100001000000 0x0 nop;(branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbug 0x4000;nop" 0b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbl 0x4000;nop" 0980100001000000 0x0 nop;(branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbul 0x4000;nop" 0780100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fblg 0x4000;nop" 0580100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbne 0x4000;nop" 0380100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbe 0x4000;nop" 1380100001000000 0x0 nop;(branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbue 0x4000;nop" 1580100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbge 0x4000;nop" 1780100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbuge 0x4000;nop" 1980100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fble 0x4000;nop" 1b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbule 0x4000;nop" 1d80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fbo 0x4000;nop" 1f80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "fba,a 0x4000;nop" 3180100001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbn,a 0x4000;nop" 2180100001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbu,a 0x4000;nop" 2f80100001000000 0x0 nop;(branch (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbg,a 0x4000;nop" 2d80100001000000 0x0 nop;(branch (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbug,a 0x4000;nop" 2b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbl,a 0x4000;nop" 2980100001000000 0x0 nop;(branch (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbul,a 0x4000;nop" 2780100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fblg,a 0x4000;nop" 2580100001000000 0x0 nop;(branch (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbne,a 0x4000;nop" 2380100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbe,a 0x4000;nop" 3380100001000000 0x0 nop;(branch (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbue,a 0x4000;nop" 3580100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbge,a 0x4000;nop" 3780100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbuge,a 0x4000;nop" 3980100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fble,a 0x4000;nop" 3b80100001000000 0x0 nop;(branch (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbule,a 0x4000;nop" 3d80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x3) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))
dE "fbo,a 0x4000;nop" 3f80100001000000 0x0 nop;(branch (|| (|| (== (bv 64 0x0) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3))) (== (bv 64 0x1) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (== (bv 64 0x2) (& (>> (var fsr) (bv 8 0xa) false) (bv 64 0x3)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x4000)))) empty (jmp (var EA))) (jmp (bv 64 0x8)))

dE "fmovrsz g1, f0, f4" 89a844a0 0x0 (branch (is_zero (var g1)) (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrdlez g1, f0, f4" 89a848c0 0x0 (branch (sle (var g1) (bv 64 0x0)) (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrqlz g1, f0, f4" 89a84ce0 0x0 (branch (&& (sle (var g1) (bv 64 0x0)) (! (== (var g1) (bv 64 0x0)))) (seq (set bv (fbits (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrsnz g1, f0, f4" 89a854a0 0x0 (branch (! (is_zero (var g1))) (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrdgz g1, f0, f4" 89a858c0 0x0 (branch (! (sle (var g1) (bv 64 0x0))) (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovrqgez g1, f0, f4" 89a85ce0 0x0 (branch (|| (! (sle (var g1) (bv 64 0x0))) (== (var g1) (bv 64 0x0))) (seq (set bv (fbits (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false)))) nop)
dE "fmovs f0, f4" 89a00020 0x0 (seq (set bv (fbits (float 0 (var f0) ))) (set f4 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmovd f0, f4" 89a00040 0x0 (seq (set bv (fbits (float 1 (append (var f0) (var f1)) ))) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmovq f0, f4" 89a00060 0x0 (seq (set bv (fbits (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ))) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f5 (cast 32 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))

dE "fadds f0, f24, f1" 83a00838 0x0 (seq (set bv (fbits (+. rna (float 0 (var f0) ) (float 0 (var f24) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fdivs f0, f24, f1" 83a009b8 0x0 (seq (set bv (fbits (/. rna (float 0 (var f0) ) (float 0 (var f24) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fsubs f0, f24, f1" 83a008b8 0x0 (seq (set bv (fbits (-. rna (float 0 (var f0) ) (float 0 (var f24) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmuls f0, f24, f1" 83a00938 0x0 (seq (set bv (fbits (*. rna (float 0 (var f0) ) (float 0 (var f24) )))) (set f1 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "faddd f0, f30, f60" bba0085e 0x0 (seq (set bv (fbits (+. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f30) (var f31)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fdivd f0, f30, f60" bba009de 0x0 (seq (set bv (fbits (/. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f30) (var f31)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fsubd f0, f30, f60" bba008de 0x0 (seq (set bv (fbits (-. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f30) (var f31)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fmuld f0, f30, f60" bba0095e 0x0 (seq (set bv (fbits (*. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f30) (var f31)) )))) (set f60 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "faddq f0, f24, f60" bba00878 0x0 (seq (set bv (fbits (+. rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ) (float 3 (append (append (append (var f24) (var f25)) (var f26)) (var f27)) )))) (set f62 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f60 (cast 64 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fdivq f0, f24, f60" bba009f8 0x0 (seq (set bv (fbits (/. rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ) (float 3 (append (append (append (var f24) (var f25)) (var f26)) (var f27)) )))) (set f62 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f60 (cast 64 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fsubq f0, f24, f60" bba008f8 0x0 (seq (set bv (fbits (-. rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ) (float 3 (append (append (append (var f24) (var f25)) (var f26)) (var f27)) )))) (set f62 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f60 (cast 64 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fmulq f0, f24, f60" bba00978 0x0 (seq (set bv (fbits (*. rna (float 3 (append (append (append (var f0) (var f1)) (var f2)) (var f3)) ) (float 3 (append (append (append (var f24) (var f25)) (var f26)) (var f27)) )))) (set f62 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f60 (cast 64 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))

dE "mova icc, g0, g1" 83660000 0x0 (branch true (set g1 (var g0)) nop)
dE "movn icc, g0, g1" 83640000 0x0 (branch false (set g1 (var g0)) nop)
dE "movne icc, g0, g1" 83664000 0x0 (branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (set g1 (var g0)) nop)
dE "move icc, g0, g1" 83644000 0x0 (branch (lsb (>> (var ccr) (bv 8 0x2) false)) (set g1 (var g0)) nop)
dE "movg icc, g0, g1" 83668000 0x0 (branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (set g1 (var g0)) nop)
dE "movle icc, g0, g1" 83648000 0x0 (branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (set g1 (var g0)) nop)
dE "movge icc, g0, g1" 8366c000 0x0 (branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (set g1 (var g0)) nop)
dE "movl icc, g0, g1" 8364c000 0x0 (branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (set g1 (var g0)) nop)
dE "movgu icc, g0, g1" 83670000 0x0 (branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (set g1 (var g0)) nop)
dE "movleu icc, g0, g1" 83650000 0x0 (branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (set g1 (var g0)) nop)
dE "movcc icc, g0, g1" 83674000 0x0 (branch (! (lsb (var ccr))) (set g1 (var g0)) nop)
dE "movcs icc, g0, g1" 83654000 0x0 (branch (lsb (var ccr)) (set g1 (var g0)) nop)
dE "movpos icc, g0, g1" 83678000 0x0 (branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (set g1 (var g0)) nop)
dE "movneg icc, g0, g1" 83658000 0x0 (branch (lsb (>> (var ccr) (bv 8 0x3) false)) (set g1 (var g0)) nop)
dE "movvc icc, g0, g1" 8367c000 0x0 (branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (set g1 (var g0)) nop)
dE "movvs icc, g0, g1" 8365c000 0x0 (branch (lsb (>> (var ccr) (bv 8 0x1) false)) (set g1 (var g0)) nop)
dE "mova xcc, 0x50, g1" 83663050 0x0 (branch true (set g1 (bv 64 0x50)) nop)
dE "movn xcc, 0x50, g1" 83643050 0x0 (branch false (set g1 (bv 64 0x50)) nop)
dE "movne xcc, 0x50, g1" 83667050 0x0 (branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false))) (set g1 (bv 64 0x50)) nop)
dE "move xcc, 0x50, g1" 83647050 0x0 (branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x2) false)) (set g1 (bv 64 0x50)) nop)
dE "movg xcc, 0x50, g1" 8366b050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (set g1 (bv 64 0x50)) nop)
dE "movle xcc, 0x50, g1" 8364b050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (set g1 (bv 64 0x50)) nop)
dE "movge xcc, 0x50, g1" 8366f050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (set g1 (bv 64 0x50)) nop)
dE "movl xcc, 0x50, g1" 8364f050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (set g1 (bv 64 0x50)) nop)
dE "movgu xcc, 0x50, g1" 83673050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (set g1 (bv 64 0x50)) nop)
dE "movleu xcc, 0x50, g1" 83653050 0x0 (branch (let ccf (>> (var ccr) (bv 8 0x4) false) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (set g1 (bv 64 0x50)) nop)
dE "movcc xcc, 0x50, g1" 83677050 0x0 (branch (! (lsb (>> (var ccr) (bv 8 0x4) false))) (set g1 (bv 64 0x50)) nop)
dE "movcs xcc, 0x50, g1" 83657050 0x0 (branch (lsb (>> (var ccr) (bv 8 0x4) false)) (set g1 (bv 64 0x50)) nop)
dE "movpos xcc, 0x50, g1" 8367b050 0x0 (branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false))) (set g1 (bv 64 0x50)) nop)
dE "movneg xcc, 0x50, g1" 8365b050 0x0 (branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x3) false)) (set g1 (bv 64 0x50)) nop)
dE "movvc xcc, 0x50, g1" 8367f050 0x0 (branch (! (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false))) (set g1 (bv 64 0x50)) nop)
dE "movvs xcc, 0x50, g1" 8365f050 0x0 (branch (lsb (>> (>> (var ccr) (bv 8 0x4) false) (bv 8 0x1) false)) (set g1 (bv 64 0x50)) nop)

dE "movrz l0, g5, g1" 837c0405 0x0 (branch (is_zero (var l0)) (set g1 (var g5)) nop)
dE "movrlez l0, g5, g1" 837c0805 0x0 (branch (sle (var l0) (bv 64 0x0)) (set g1 (var g5)) nop)
dE "movrlz l0, g5, g1" 837c0c05 0x0 (branch (&& (sle (var l0) (bv 64 0x0)) (! (== (var l0) (bv 64 0x0)))) (set g1 (var g5)) nop)
dE "movrnz l0, g5, g1" 837c1405 0x0 (branch (! (is_zero (var l0))) (set g1 (var g5)) nop)
dE "movrgz l0, g5, g1" 837c1805 0x0 (branch (! (sle (var l0) (bv 64 0x0))) (set g1 (var g5)) nop)
dE "movrgez l0, g5, g1" 837c1c05 0x0 (branch (|| (! (sle (var l0) (bv 64 0x0))) (== (var l0) (bv 64 0x0))) (set g1 (var g5)) nop)
dE "movrz l0, 0x10, g1" 837c2410 0x0 (branch (is_zero (var l0)) (set g1 (bv 64 0x10)) nop)
dE "movrlez l0, 0x10, g1" 837c2810 0x0 (branch (sle (var l0) (bv 64 0x0)) (set g1 (bv 64 0x10)) nop)
dE "movrlz l0, 0x10, g1" 837c2c10 0x0 (branch (&& (sle (var l0) (bv 64 0x0)) (! (== (var l0) (bv 64 0x0)))) (set g1 (bv 64 0x10)) nop)
dE "movrnz l0, 0x10, g1" 837c3410 0x0 (branch (! (is_zero (var l0))) (set g1 (bv 64 0x10)) nop)
dE "movrgz l0, 0x10, g1" 837c3810 0x0 (branch (! (sle (var l0) (bv 64 0x0))) (set g1 (bv 64 0x10)) nop)
dE "movrgez l0, 0x10, g1" 837c3c10 0x0 (branch (|| (! (sle (var l0) (bv 64 0x0))) (== (var l0) (bv 64 0x0))) (set g1 (bv 64 0x10)) nop)

# Registers f32-f63 are not defined in Capstone in those names.
# Test if they are properly resolved.
dE "ldq [g1], f32" c3104000 0x0 (seq (set load (loadw 0 128 (var g1))) (set f34 (cast 64 false (var load))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f32 (cast 64 false (>> (var load) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "stq f32, [g1]" c3304000 0x0 (storew 0 (var g1) (append (var f32) (var f34)))
dE "ldd [g1], f60" fb184000 0x0 (seq (set f60 (loadw 0 64 (var g1))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "std f60, [g1]" fb384000 0x0 (storew 0 (var g1) (var f60))

dE "sllx g1, g2, g3" 87285002 0x0 (set g3 (cast 64 false (<< (cast 64 false (var g1)) (cast 6 false (var g2)) false)))
dE "sllx g1, 0x3f, g3" 8728703f 0x0 (set g3 (cast 64 false (<< (cast 64 false (var g1)) (cast 6 false (bv 64 0x3f)) false)))
dE "srlx g1, g2, g3" 87305002 0x0 (set g3 (cast 64 false (>> (cast 64 false (var g1)) (cast 6 false (var g2)) false)))
dE "srlx g1, 0x3f, g3" 8730703f 0x0 (set g3 (cast 64 false (>> (cast 64 false (var g1)) (cast 6 false (bv 64 0x3f)) false)))
dE "srax g1, g2, g3" 87385002 0x0 (set g3 (cast 64 false (>> (cast 64 false (var g1)) (cast 6 false (var g2)) (msb (cast 64 false (var g1))))))
dE "srax g1, 0x3f, g3" 8738703f 0x0 (set g3 (cast 64 false (>> (cast 64 false (var g1)) (cast 6 false (bv 64 0x3f)) (msb (cast 64 false (var g1))))))

dE "stq f0, [i0+l6]" c1360016 0x0 (storew 0 (+ (var i0) (var l6)) (append (var f0) (append (var f1) (append (var f2) (var f3)))))
dE "stq f0, [i0+0x20]" c1362020 0x0 (storew 0 (+ (var i0) (bv 64 0x20)) (append (var f0) (append (var f1) (append (var f2) (var f3)))))
dE "stq f0, [g1]" c1304000 0x0 (storew 0 (var g1) (append (var f0) (append (var f1) (append (var f2) (var f3)))))
dE "stqa f0, [i0+l6] 0x40" c1b60816 0x0 (storew 0 (+ (var i0) (var l6)) (append (var f0) (append (var f1) (append (var f2) (var f3)))))
dE "stqa f0, [g1] 0x40" c1b04800 0x0 (storew 0 (var g1) (append (var f0) (append (var f1) (append (var f2) (var f3)))))

dE "ldd [g1], f0" c1184000 0x0 (seq (set load (loadw 0 64 (var g1))) (set f1 (cast 32 false (var load))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var load) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "ldq [g1], f0" c1104000 0x0 (seq (set load (loadw 0 128 (var g1))) (set f3 (cast 32 false (var load))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f2 (cast 32 false (>> (var load) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f1 (cast 32 false (>> (var load) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var load) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "ldstub [i0+l6], o2" d46e0016 0x0 (seq (set o2 (cast 64 false (loadw 0 8 (+ (var i0) (var l6))))) (storew 0 (+ (var i0) (var l6)) (bv 8 0xff)))
dE "ldda [g1] 1, f0" c1984020 0x0 (seq (set load (loadw 0 64 (var g1))) (set f1 (cast 32 false (var load))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var load) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "ldqa [g1] 1, f0" c1904020 0x0 (seq (set load (loadw 0 128 (var g1))) (set f3 (cast 32 false (var load))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f2 (cast 32 false (>> (var load) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f1 (cast 32 false (>> (var load) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f0 (cast 32 false (>> (var load) (bv 8 0x60) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "ldd [g1], f60" fb184000 0x0 (seq (set f60 (loadw 0 64 (var g1))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))

dE "umulxhi l1, l2, l3" a7b442d2 0x0 (seq (set res128 (* (cast 128 false (cast 64 false (var l1))) (cast 128 false (cast 64 false (var l2))))) (set l3 (cast 64 false (>> (var res128) (bv 8 0x40) false))))
dE "mulx g1, i2, i0" b048401a 0x0 (set i0 (cast 64 false (* (cast 64 false (var g1)) (cast 64 false (var i2)))))
dE "mulx g1, 0x3f, i0" b048603f 0x0 (set i0 (cast 64 false (* (cast 64 false (var g1)) (cast 64 false (bv 64 0x3f)))))
dE "sdivx g1, i2, i0" b168401a 0x0 (set i0 (cast 64 false (sdiv (cast 64 false (var g1)) (cast 64 false (var i2)))))
dE "sdivx g1, 0x3f, i0" b168603f 0x0 (set i0 (cast 64 false (sdiv (cast 64 false (var g1)) (cast 64 false (bv 64 0x3f)))))
dE "udivx g1, i2, i0" b068401a 0x0 (set i0 (cast 64 false (div (cast 64 false (var g1)) (cast 64 false (var i2)))))
dE "udivx g1, 0x3f, i0" b068603f 0x0 (set i0 (cast 64 false (div (cast 64 false (var g1)) (cast 64 false (bv 64 0x3f)))))
dE "ba icc, 0x1000;nop" 1048040001000000 0x0 nop;(branch true (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bn icc, 0x1000;nop" 0048040001000000 0x0 nop;(branch false (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bne icc, 0x1000;nop" 1248040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "be icc, 0x1000;nop" 0248040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bg icc, 0x1000;nop" 1448040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "ble icc, 0x1000;nop" 0448040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (>> (var ccf) (bv 8 0x2) false)) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bge icc, 0x1000;nop" 1648040001000000 0x0 nop;(branch (let ccf (var ccr) (! (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bl icc, 0x1000;nop" 0648040001000000 0x0 nop;(branch (let ccf (var ccr) (^^ (lsb (>> (var ccf) (bv 8 0x3) false)) (lsb (>> (var ccf) (bv 8 0x1) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bgu icc, 0x1000;nop" 1848040001000000 0x0 nop;(branch (let ccf (var ccr) (! (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false))))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bleu icc, 0x1000;nop" 0848040001000000 0x0 nop;(branch (let ccf (var ccr) (|| (lsb (var ccf)) (lsb (>> (var ccf) (bv 8 0x2) false)))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcc icc, 0x1000;nop" 1a48040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bcs icc, 0x1000;nop" 0a48040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bpos icc, 0x1000;nop" 1c48040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bneg icc, 0x1000;nop" 0c48040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvc icc, 0x1000;nop" 1e48040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "bvs icc, 0x1000;nop" 0e48040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 64 false (cast 64 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 64 0x4)))
dE "swap [i0+l6], o2" d47e0016 0x0 (seq (set mem_val (loadw 0 32 (+ (var i0) (var l6)))) (storew 0 (+ (var i0) (var l6)) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val))))
dE "swap [i0+0x20], o2" d47e2020 0x0 (seq (set mem_val (loadw 0 32 (+ (var i0) (bv 64 0x20)))) (storew 0 (+ (var i0) (bv 64 0x20)) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val))))
dE "cas [i0], l6, o2" d5e61016 0x0 (seq (set mem_val (loadw 0 32 (var i0))) (branch (== (var mem_val) (cast 32 false (var l6))) (seq (storew 0 (var i0) (cast 32 false (var o2))) (set o2 (cast 64 false (var mem_val)))) (set o2 (cast 64 false (var mem_val)))))
dE "casx [i0], l6, o2" d5f61016 0x0 (seq (set mem_val (loadw 0 64 (var i0))) (branch (== (var mem_val) (var l6)) (seq (storew 0 (var i0) (var o2)) (set o2 (var mem_val))) (set o2 (var mem_val))))
dE "movdtox f32, i0" b1b02201 0x0 (set i0 (fbits (float 1 (var f32) )))
dE "movdtox f0, i0" b1b02200 0x0 (set i0 (fbits (float 1 (append (var f0) (var f1)) )))
dE "movstouw f0, i0" b1b02220 0x0 (set i0 (cast 64 false (fbits (float 0 (var f0) ))))
dE "movstosw f0, i0" b1b02260 0x0 (set i0 (cast 64 (msb (fbits (float 0 (var f0) ))) (fbits (float 0 (var f0) ))))
dE "xmulx l0, l1, l2" a5b422b1 0x0 (seq (set res128 (bv 128 0x0)) (set rs1 (cast 128 false (cast 64 false (var l0)))) (set rs2 (cast 128 false (cast 64 false (var l1)))) (set i (bv 8 0x0)) (repeat (&& (ule (var i) (bv 8 0x40)) (! (== (var i) (bv 8 0x40)))) (seq (set res128 (^ (var res128) (ite (lsb (>> (var rs2) (var i) false)) (<< (var rs1) (var i) false) (bv 128 0x0)))) (set i (+ (var i) (bv 8 0x1))))) (set l2 (cast 64 false (var res128))))
dE "xmulxhi l0, l1, l2" a5b422d1 0x0 (seq (set res128 (bv 128 0x0)) (set rs1 (cast 128 false (cast 64 false (var l0)))) (set rs2 (cast 128 false (cast 64 false (var l1)))) (set i (bv 8 0x0)) (repeat (&& (ule (var i) (bv 8 0x40)) (! (== (var i) (bv 8 0x40)))) (seq (set res128 (^ (var res128) (ite (lsb (>> (var rs2) (var i) false)) (<< (var rs1) (var i) false) (bv 128 0x0)))) (set i (+ (var i) (bv 8 0x1))))) (set l2 (cast 64 false (>> (var res128) (bv 8 0x40) false))))
dE "fhadds f0, f4, f8" 91a00c24 0x0 (seq (set bv (fbits (/. rna (+. rna (float 0 (var f0) ) (float 0 (var f4) )) (fcast_float ieee754-bin32 rna (bv 32 0x2))))) (set f8 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fhaddd f0, f4, f8" 91a00c44 0x0 (seq (set bv (fbits (/. rna (+. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f4) (var f5)) )) (fcast_float ieee754-bin64 rna (bv 64 0x2))))) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnhadds f0, f4, f8" 91a00e24 0x0 (seq (set bv (fbits (fneg (/. rna (+. rna (float 0 (var f0) ) (float 0 (var f4) )) (fcast_float ieee754-bin32 rna (bv 32 0x2)))))) (set f8 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnhaddd f0, f4, f8" 91a00e44 0x0 (seq (set bv (fbits (fneg (/. rna (+. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f4) (var f5)) )) (fcast_float ieee754-bin64 rna (bv 64 0x2)))))) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fhsubs f0, f4, f8" 91a00ca4 0x0 (seq (set bv (fbits (/. rna (-. rna (float 0 (var f0) ) (float 0 (var f4) )) (fcast_float ieee754-bin32 rna (bv 32 0x2))))) (set f8 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fhsubd f0, f4, f8" 91a00cc4 0x0 (seq (set bv (fbits (/. rna (-. rna (float 1 (append (var f0) (var f1)) ) (float 1 (append (var f4) (var f5)) )) (fcast_float ieee754-bin64 rna (bv 64 0x2))))) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnadds f0, f4, f8" 91a00a24 0x0 (seq (set bv (fbits (fneg (+. rna (float 0 (var f0) ) (float 0 (var f4) ))))) (set f8 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fnaddd f32, f34, f36" 8ba04a43 0x0 (seq (set bv (fbits (fneg (+. rna (float 1 (var f32) ) (float 1 (var f34) ))))) (set f36 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fsmuld f0, f4, f8" 91a00d24 0x0 (seq (set bv (fbits (*. rna (fconvert ieee754-bin64 rna (float 0 (var f0) )) (fconvert ieee754-bin64 rna (float 0 (var f4) ))))) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fdmulq f32, f34, f36" 8ba04dc3 0x0 (seq (set bv (fbits (*. rna (fconvert ieee754-bin128 rna (float 1 (var f32) )) (fconvert ieee754-bin128 rna (float 1 (var f34) ))))) (set f38 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))) (set f36 (cast 64 false (>> (var bv) (bv 8 0x40) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fpadd16 f0, f4, f16" a1b00a04 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set res (| (var res) (<< (cast 64 false (cast 16 false (+ (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (+ (>> (var rs1) (bv 8 0x10) false) (>> (var rs2) (bv 8 0x10) false)))) (bv 8 0x10) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (+ (>> (var rs1) (bv 8 0x20) false) (>> (var rs2) (bv 8 0x20) false)))) (bv 8 0x20) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (+ (>> (var rs1) (bv 8 0x30) false) (>> (var rs2) (bv 8 0x30) false)))) (bv 8 0x30) false))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpsub16 f0, f4, f16" a1b00a84 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set res (| (var res) (<< (cast 64 false (cast 16 false (- (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (- (>> (var rs1) (bv 8 0x10) false) (>> (var rs2) (bv 8 0x10) false)))) (bv 8 0x10) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (- (>> (var rs1) (bv 8 0x20) false) (>> (var rs2) (bv 8 0x20) false)))) (bv 8 0x20) false))) (set res (| (var res) (<< (cast 64 false (cast 16 false (- (>> (var rs1) (bv 8 0x30) false) (>> (var rs2) (bv 8 0x30) false)))) (bv 8 0x30) false))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpadd16s f0, f4, f16" a1b00a24 0x0 (seq (set res (bv 32 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f4) ))) (set res (| (var res) (<< (cast 32 false (cast 16 false (+ (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 32 false (cast 16 false (+ (>> (var rs1) (bv 8 0x10) false) (>> (var rs2) (bv 8 0x10) false)))) (bv 8 0x10) false))) (set bv (var res)) (set f16 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpsub16s f0, f4, f16" a1b00aa4 0x0 (seq (set res (bv 32 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f4) ))) (set res (| (var res) (<< (cast 32 false (cast 16 false (- (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 32 false (cast 16 false (- (>> (var rs1) (bv 8 0x10) false) (>> (var rs2) (bv 8 0x10) false)))) (bv 8 0x10) false))) (set bv (var res)) (set f16 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpadd32 f0, f4, f16" a1b00a44 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set res (| (var res) (<< (cast 64 false (cast 32 false (+ (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (cast 32 false (+ (>> (var rs1) (bv 8 0x20) false) (>> (var rs2) (bv 8 0x20) false)))) (bv 8 0x20) false))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpsub32 f0, f4, f16" a1b00ac4 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set res (| (var res) (<< (cast 64 false (cast 32 false (- (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set res (| (var res) (<< (cast 64 false (cast 32 false (- (>> (var rs1) (bv 8 0x20) false) (>> (var rs2) (bv 8 0x20) false)))) (bv 8 0x20) false))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpadd32s f0, f4, f16" a1b00a64 0x0 (seq (set res (bv 32 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f4) ))) (set res (| (var res) (<< (cast 32 false (cast 32 false (+ (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set bv (var res)) (set f16 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpsub32s f0, f4, f16" a1b00ae4 0x0 (seq (set res (bv 32 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f4) ))) (set res (| (var res) (<< (cast 32 false (cast 32 false (- (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set bv (var res)) (set f16 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fpadd64 f0, f4, f16" a1b00844 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set res (| (var res) (<< (cast 64 false (cast 64 false (+ (>> (var rs1) (bv 8 0x0) false) (>> (var rs2) (bv 8 0x0) false)))) (bv 8 0x0) false))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmul8x16 f0, f4, f16" a1b00624 0x0 (seq (set res (bv 64 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (set m (cast 64 false (>> (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x0) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x0) false)) (>> (var rs2) (bv 8 0x0) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x0) false)) (>> (var rs2) (bv 8 0x0) false)))) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x0) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x0) false)) (>> (var rs2) (bv 8 0x0) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x0) false)) (>> (var rs2) (bv 8 0x0) false)))) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x0) false))) (& (<< (var m) (bv 8 0x0) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x0) false)))) (set m (cast 64 false (>> (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x8) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x10) false)) (>> (var rs2) (bv 8 0x10) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x10) false)) (>> (var rs2) (bv 8 0x10) false)))) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x8) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x10) false)) (>> (var rs2) (bv 8 0x10) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x10) false)) (>> (var rs2) (bv 8 0x10) false)))) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x10) false))) (& (<< (var m) (bv 8 0x10) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x10) false)))) (set m (cast 64 false (>> (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x10) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x20) false)) (>> (var rs2) (bv 8 0x20) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x20) false)) (>> (var rs2) (bv 8 0x20) false)))) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x10) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x20) false)) (>> (var rs2) (bv 8 0x20) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x20) false)) (>> (var rs2) (bv 8 0x20) false)))) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x20) false))) (& (<< (var m) (bv 8 0x20) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x20) false)))) (set m (cast 64 false (>> (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x18) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x30) false)) (>> (var rs2) (bv 8 0x30) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x30) false)) (>> (var rs2) (bv 8 0x30) false)))) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (cast 32 false (cast 8 false (>> (var rs1) (bv 8 0x18) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (bv 8 0x30) false)) (>> (var rs2) (bv 8 0x30) false))) (cast 16 (msb (>> (var rs2) (bv 8 0x30) false)) (>> (var rs2) (bv 8 0x30) false)))) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x30) false))) (& (<< (var m) (bv 8 0x30) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (bv 8 0x30) false)))) (set bv (var res)) (set f17 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f16 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmul8x16al f0, f4, f32" 83b006a4 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (cast 32 false (fbits (float 0 (var f0) )))) (set rs2 (cast 32 (msb (cast 16 (msb (fbits (float 0 (var f4) ))) (fbits (float 0 (var f4) )))) (cast 16 (msb (fbits (float 0 (var f4) ))) (fbits (float 0 (var f4) ))))) (repeat (&& (ule (var i) (bv 8 0x4)) (! (== (var i) (bv 8 0x4)))) (seq (set m (cast 64 false (>> (+ (* (& (bv 32 0xff) (>> (var rs1) (* (bv 8 0x8) (var i)) false)) (var rs2)) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (& (bv 32 0xff) (>> (var rs1) (* (bv 8 0x8) (var i)) false)) (var rs2)) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false))) (& (<< (var m) (* (bv 8 0x10) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fmul8x16au f0, f4, f32" 83b00664 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (cast 32 false (fbits (float 0 (var f0) )))) (set rs2 (cast 32 (msb (cast 16 (msb (>> (fbits (float 0 (var f4) )) (bv 8 0x10) false)) (>> (fbits (float 0 (var f4) )) (bv 8 0x10) false))) (cast 16 (msb (>> (fbits (float 0 (var f4) )) (bv 8 0x10) false)) (>> (fbits (float 0 (var f4) )) (bv 8 0x10) false)))) (repeat (&& (ule (var i) (bv 8 0x4)) (! (== (var i) (bv 8 0x4)))) (seq (set m (cast 64 false (>> (+ (* (& (bv 32 0xff) (>> (var rs1) (* (bv 8 0x8) (var i)) false)) (var rs2)) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (& (bv 32 0xff) (>> (var rs1) (* (bv 8 0x8) (var i)) false)) (var rs2)) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false))) (& (<< (var m) (* (bv 8 0x10) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fmul8sux16 f0, f2, f4" 89b006c2 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var i) (bv 8 0x4)) (! (== (var i) (bv 8 0x4)))) (seq (set m (cast 64 false (>> (+ (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (+ (bv 8 0x8) (* (bv 8 0x10) (var i))) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false)))) (bv 32 0x80)) (bv 8 0x8) (msb (+ (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (+ (bv 8 0x8) (* (bv 8 0x10) (var i))) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false)))) (bv 32 0x80)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false))) (& (<< (var m) (* (bv 8 0x10) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmul8ulx16 f0, f2, f6" 8db006e2 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var i) (bv 8 0x4)) (! (== (var i) (bv 8 0x4)))) (seq (set m (cast 64 false (>> (+ (cast 32 (msb (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x10) (var i)) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))))) (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x10) (var i)) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))))) (bv 32 0x8000)) (bv 8 0x10) (msb (+ (cast 32 (msb (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x10) (var i)) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))))) (* (cast 32 false (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x10) (var i)) false))) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))))) (bv 32 0x8000)))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false))) (& (<< (var m) (* (bv 8 0x10) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x10)) false) (* (bv 8 0x10) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmuld8sux16 f0, f2, f4" 89b00702 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f2) ))) (repeat (&& (ule (var i) (bv 8 0x2)) (! (== (var i) (bv 8 0x2)))) (seq (set m (<< (* (& (bv 32 0xff) (>> (var rs1) (+ (bv 8 0x8) (* (bv 8 0x10) (var i))) false)) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false)))) (bv 8 0x8) false)) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x20)) false) (* (bv 8 0x20) (var i)) false))) (& (<< (cast 64 false (var m)) (* (bv 8 0x20) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x20)) false) (* (bv 8 0x20) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmuld8ulx16 f0, f2, f6" 8db00722 0x0 (seq (set i (bv 8 0x0)) (set res (bv 64 0x0)) (set rs1 (fbits (float 0 (var f0) ))) (set rs2 (fbits (float 0 (var f2) ))) (repeat (&& (ule (var i) (bv 8 0x2)) (! (== (var i) (bv 8 0x2)))) (seq (set m (* (& (bv 32 0xff) (>> (var rs1) (* (bv 8 0x10) (var i)) false)) (cast 32 (msb (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))) (cast 16 (msb (>> (var rs2) (* (bv 8 0x10) (var i)) false)) (>> (var rs2) (* (bv 8 0x10) (var i)) false))))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x20)) false) (* (bv 8 0x20) (var i)) false))) (& (<< (cast 64 false (var m)) (* (bv 8 0x20) (var i)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x20)) false) (* (bv 8 0x20) (var i)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var res)) (set f7 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f6 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "alignaddr l0, l1, l2" a5b40311 0x0 (seq (set addr (+ (var l0) (var l1))) (set gsr (| (& (var gsr) (bv 64 0xfffffffffffffff8)) (& (var addr) (bv 64 0x7)))) (set l2 (& (var addr) (bv 64 0xfffffffffffffff8))))
dE "alignaddrl l0, l1, l2" a5b40351 0x0 (seq (set addr (+ (var l0) (var l1))) (set gsr (| (& (var gsr) (bv 64 0xfffffffffffffff8)) (& (~- (& (var addr) (bv 64 0x7))) (bv 64 0x7)))) (set l2 (& (var addr) (bv 64 0xfffffffffffffff8))))
dE "fpmerge f0, f2, f8" 91b00962 0x0 (seq (set res (bv 64 0x0)) (set rs1 (cast 64 false (fbits (float 0 (var f0) )))) (set rs2 (cast 64 false (fbits (float 0 (var f2) )))) (set res (| (| (var res) (<< (& (>> (var rs1) (bv 8 0x0) false) (bv 64 0xff)) (bv 8 0x8) false)) (<< (& (>> (var rs2) (bv 8 0x0) false) (bv 64 0xff)) (bv 8 0x0) false))) (set res (| (| (var res) (<< (& (>> (var rs1) (bv 8 0x8) false) (bv 64 0xff)) (bv 8 0x18) false)) (<< (& (>> (var rs2) (bv 8 0x8) false) (bv 64 0xff)) (bv 8 0x10) false))) (set res (| (| (var res) (<< (& (>> (var rs1) (bv 8 0x10) false) (bv 64 0xff)) (bv 8 0x28) false)) (<< (& (>> (var rs2) (bv 8 0x10) false) (bv 64 0xff)) (bv 8 0x20) false))) (set res (| (| (var res) (<< (& (>> (var rs1) (bv 8 0x18) false) (bv 64 0xff)) (bv 8 0x38) false)) (<< (& (>> (var rs2) (bv 8 0x18) false) (bv 64 0xff)) (bv 8 0x30) false))) (set bv (var res)) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fexpand f2, f8" 91b009a2 0x0 (seq (set res (bv 64 0x0)) (set rs2 (cast 64 false (fbits (float 0 (var f2) )))) (set res (| (var res) (<< (& (>> (var rs2) (bv 8 0x0) false) (bv 64 0xff)) (bv 8 0x4) false))) (set res (| (var res) (<< (& (>> (var rs2) (bv 8 0x8) false) (bv 64 0xff)) (bv 8 0x14) false))) (set res (| (var res) (<< (& (>> (var rs2) (bv 8 0x10) false) (bv 64 0xff)) (bv 8 0x24) false))) (set res (| (var res) (<< (& (>> (var rs2) (bv 8 0x18) false) (bv 64 0xff)) (bv 8 0x34) false))) (set bv (var res)) (set f9 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f8 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "popc l2, l6" ad700012 0x0 (seq (set i (bv 8 0x0)) (set c (bv 64 0x0)) (set rs1 (cast 64 false (var l2))) (repeat (&& (ule (var i) (bv 8 0x40)) (! (== (var i) (bv 8 0x40)))) (seq (set i (+ (var i) (bv 8 0x1))) (set c (+ (var c) (ite (lsb (var rs1)) (bv 64 0x1) (bv 64 0x0)))) (set rs1 (>> (var rs1) (bv 8 0x1) false)))) (set l6 (cast 64 false (var c))))
dE "lzcnt l2, l6" adb002f2 0x0 (seq (set c (bv 64 0x0)) (set rs1 (cast 64 false (var l2))) (repeat (&& (! (msb (var rs1))) (&& (ule (var c) (bv 64 0x40)) (! (== (var c) (bv 64 0x40))))) (seq (set c (+ (var c) (bv 64 0x1))) (set rs1 (<< (var rs1) (bv 8 0x1) false)))) (set l6 (cast 64 false (var c))))
dE "tsubcc l0, l2, l6" ad0c0012 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var l0)))) (set arg1 (cast 128 false (cast 64 false (var l2)))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set l6 (cast 64 false (var res128))) (set ccr (ite (ite (|| (|| (! (is_zero (& (cast 64 false (var l0)) (bv 64 0x3)))) (! (is_zero (& (cast 64 false (var l2)) (bv 64 0x3))))) (lsb (>> (var ccr) (bv 8 0x1) false))) true false) (| (var ccr) (bv 8 0x2)) (& (var ccr) (~ (bv 8 0x2))))))
dE "taddcc l0, l2, l6" ad040012 0x0 (seq (set arg0 (cast 128 false (cast 64 false (var l0)))) (set arg1 (cast 128 false (cast 64 false (var l2)))) (set res128_mid (+ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (! (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1))))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (! (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1))))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (^^ (^^ (msb (cast 33 false (var arg0))) (msb (cast 33 false (var arg1)))) (msb (cast 33 false (var res128))))) (set carry64 (msb (cast 65 false (var res128)))) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set l6 (cast 64 false (var res128))) (set ccr (ite (ite (|| (|| (! (is_zero (& (cast 64 false (var l0)) (bv 64 0x3)))) (! (is_zero (& (cast 64 false (var l2)) (bv 64 0x3))))) (lsb (>> (var ccr) (bv 8 0x1) false))) true false) (| (var ccr) (bv 8 0x2)) (& (var ccr) (~ (bv 8 0x2))))))
dE "tsubcctv l0, l2, l6" ad1c0012 0x0 (branch (ite (|| (|| (! (is_zero (& (cast 64 false (var l0)) (bv 64 0x3)))) (! (is_zero (& (cast 64 false (var l2)) (bv 64 0x3))))) (&& (^^ (msb (cast 32 false (cast 64 false (var l0)))) (msb (cast 32 false (cast 64 false (var l2))))) (^^ (msb (cast 32 false (cast 64 false (var l0)))) (msb (- (cast 64 false (var l0)) (cast 64 false (var l0))))))) true false) (goto trap) (seq (set arg0 (cast 128 false (cast 64 false (var l0)))) (set arg1 (cast 128 false (cast 64 false (var l2)))) (set res128_mid (- (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1)))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1)))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (|| (&& (ule (cast 32 false (var arg0)) (cast 32 false (var arg1))) (! (== (cast 32 false (var arg0)) (cast 32 false (var arg1))))) false)) (set carry64 (|| (&& (ule (cast 64 false (var arg0)) (cast 64 false (var arg1))) (! (== (cast 64 false (var arg0)) (cast 64 false (var arg1))))) false)) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set l6 (cast 64 false (var res128)))))
dE "taddcctv l0, l2, l6" ad140012 0x0 (branch (ite (|| (|| (! (is_zero (& (cast 64 false (var l0)) (bv 64 0x3)))) (! (is_zero (& (cast 64 false (var l2)) (bv 64 0x3))))) (&& (! (^^ (msb (cast 32 false (cast 64 false (var l0)))) (msb (cast 32 false (cast 64 false (var l2)))))) (^^ (msb (cast 32 false (cast 64 false (var l0)))) (msb (+ (cast 64 false (var l0)) (cast 64 false (var l0))))))) true false) (goto trap) (seq (set arg0 (cast 128 false (cast 64 false (var l0)))) (set arg1 (cast 128 false (cast 64 false (var l2)))) (set res128_mid (+ (var arg0) (var arg1))) (set res128 (var res128_mid)) (set is_zero32 (is_zero (cast 32 false (var res128)))) (set is_zero64 (is_zero (cast 64 false (var res128)))) (set is_neg32 (msb (cast 32 false (var res128)))) (set is_neg64 (msb (cast 64 false (var res128)))) (set overflow32 (&& (! (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var arg1))))) (^^ (msb (cast 32 false (var arg0))) (msb (cast 32 false (var res128)))))) (set overflow64 (&& (! (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var arg1))))) (^^ (msb (cast 64 false (var arg0))) (msb (cast 64 false (var res128)))))) (set carry32 (^^ (^^ (msb (cast 33 false (var arg0))) (msb (cast 33 false (var arg1)))) (msb (cast 33 false (var res128))))) (set carry64 (msb (cast 65 false (var res128)))) (set ccr (| (ite (var carry32) (bv 8 0x1) (bv 8 0x0)) (| (<< (ite (var overflow32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false) (| (<< (ite (var is_zero32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false) (| (<< (ite (var is_neg32) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false) (| (<< (ite (var carry64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x4) false) (| (<< (ite (var overflow64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x5) false) (| (<< (ite (var is_zero64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x6) false) (<< (ite (var is_neg64) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x7) false))))))))) (set l6 (cast 64 false (var res128)))))
dE "faligndata f0, f32, f34" 87b00901 0x0 (seq (set data (append (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (var f32) )))) (set f34 (cast 64 false (>> (var data) (* (- (bv 8 0x8) (cast 8 false (cast 3 false (var gsr)))) (bv 8 0x8)) false))))
dE "pdistn f0, f4, l6" adb007e4 0x0 (seq (set dst (bv 64 0x0)) (set c (bv 8 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (repeat (&& (ule (var c) (bv 8 0x8)) (! (== (var c) (bv 8 0x8)))) (seq (set sub (- (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x8) (var c)) false)) (& (bv 64 0xff) (>> (var rs2) (* (bv 8 0x8) (var c)) false)))) (set dst (+ (var dst) (ite (&& (sle (var sub) (bv 64 0x0)) (! (== (var sub) (bv 64 0x0)))) (~- (var sub)) (var sub)))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var dst)) (set l6 (cast 64 false (var bv))))
dE "pdist f0, f32, f34" 87b007c1 0x0 (seq (set dst (fbits (float 1 (var f34) ))) (set c (bv 8 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (var f32) ))) (repeat (&& (ule (var c) (bv 8 0x8)) (! (== (var c) (bv 8 0x8)))) (seq (set sub (- (& (bv 64 0xff) (>> (var rs1) (* (bv 8 0x8) (var c)) false)) (& (bv 64 0xff) (>> (var rs2) (* (bv 8 0x8) (var c)) false)))) (set dst (+ (var dst) (ite (&& (sle (var sub) (bv 64 0x0)) (! (== (var sub) (bv 64 0x0)))) (~- (var sub)) (var sub)))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var dst)) (set f34 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "bmask l0, l1, l3" a7b40331 0x0 (seq (set res (+ (var l0) (var l1))) (set l3 (var res)) (set gsr (| (& (var gsr) (bv 64 0xffffffff)) (<< (var res) (bv 8 0x20) false))))
dE "bshuffle f0, f2, f4" 89b00982 0x0 (seq (set dst (bv 64 0x0)) (set mask (>> (var gsr) (bv 8 0x20) false)) (set i (bv 8 0x0)) (set src (append (fbits (float 1 (append (var f0) (var f1)) )) (fbits (float 1 (append (var f2) (var f3)) )))) (repeat (&& (ule (var i) (bv 8 0x8)) (! (== (var i) (bv 8 0x8)))) (seq (set src_byte_idx (cast 8 false (& (bv 64 0xf) (>> (var mask) (- (bv 8 0x1c) (* (var i) (bv 8 0x4))) false)))) (set src_byte (cast 8 false (>> (var src) (- (bv 8 0x78) (* (var src_byte_idx) (bv 8 0x8))) false))) (set dst (| (& (var dst) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x8)) false) (* (var i) (bv 8 0x8)) false))) (& (<< (cast 64 false (var src_byte)) (* (var i) (bv 8 0x8)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x8)) false) (* (var i) (bv 8 0x8)) false)))) (set i (+ (var i) (bv 8 0x1))))) (set bv (var dst)) (set f5 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))) (set f4 (cast 32 false (>> (var bv) (bv 8 0x20) false))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "fmean16 f0, f2, f32" 83b00802 0x0 (seq (set res (bv 64 0x0)) (set c (bv 8 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var c) (bv 8 0x4)) (! (== (var c) (bv 8 0x4)))) (seq (set op1 (cast 16 (msb (>> (var rs1) (* (var c) (bv 8 0x10)) false)) (>> (var rs1) (* (var c) (bv 8 0x10)) false))) (set op2 (cast 16 (msb (>> (var rs2) (* (var c) (bv 8 0x10)) false)) (>> (var rs2) (* (var c) (bv 8 0x10)) false))) (set part_res (cast 16 false (>> (+ (+ (cast 17 (msb (var op1)) (var op1)) (cast 17 (msb (var op2)) (var op2))) (bv 17 0x1)) (bv 8 0x1) false))) (set res (| (var res) (<< (cast 64 false (var part_res)) (* (var c) (bv 8 0x10)) false))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var res)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fchksm16 f0, f2, f32" 83b00882 0x0 (seq (set res (bv 64 0x0)) (set c (bv 8 0x0)) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var c) (bv 8 0x4)) (! (== (var c) (bv 8 0x4)))) (seq (set op1 (cast 16 false (>> (var rs1) (* (var c) (bv 8 0x10)) false))) (set op2 (cast 16 false (>> (var rs2) (* (var c) (bv 8 0x10)) false))) (set interm_sum (+ (cast 17 false (var op1)) (cast 17 false (var op2)))) (set sum (ite (msb (var interm_sum)) (cast 16 false (+ (var interm_sum) (bv 17 0x1))) (cast 16 false (var interm_sum)))) (set res (| (var res) (<< (cast 64 false (var sum)) (* (var c) (bv 8 0x10)) false))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var res)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fpack16 f2, f32" 83b00762 0x0 (seq (set res (bv 32 0x0)) (set c (bv 8 0x0)) (set scale (cast 8 false (cast 4 false (>> (var gsr) (bv 8 0x3) false)))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var c) (bv 8 0x4)) (! (== (var c) (bv 8 0x4)))) (seq (set part (cast 16 (msb (>> (var rs2) (* (var c) (bv 8 0x10)) false)) (>> (var rs2) (* (var c) (bv 8 0x10)) false))) (set scaled_part (>> (<< (cast 32 (msb (var part)) (var part)) (var scale) false) (bv 8 0x7) (msb (<< (cast 32 (msb (var part)) (var part)) (var scale) false)))) (set truncated (& (ite (&& (sle (var scaled_part) (bv 32 0x0)) (! (== (var scaled_part) (bv 32 0x0)))) (bv 32 0x0) (ite (! (sle (var scaled_part) (bv 32 0xff))) (bv 32 0xff) (var scaled_part))) (bv 32 0xff))) (set res (| (& (var res) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (* (var c) (bv 8 0x8)) false))) (& (<< (var truncated) (* (var c) (bv 8 0x8)) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x8)) false) (* (var c) (bv 8 0x8)) false)))) (set c (+ (var c) (bv 8 0x1))))) (set f32 (cast 64 false (var res))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fpack32 f0, f2, f32" 83b00742 0x0 (seq (set res (bv 64 0x0)) (set c (bv 8 0x0)) (set scale (cast 8 false (cast 5 false (>> (var gsr) (bv 8 0x3) false)))) (set rs1 (fbits (float 1 (append (var f0) (var f1)) ))) (set rs2 (fbits (float 1 (append (var f2) (var f3)) ))) (repeat (&& (ule (var c) (bv 8 0x2)) (! (== (var c) (bv 8 0x2)))) (seq (set part (cast 32 (msb (>> (var rs2) (* (var c) (bv 8 0x20)) false)) (>> (var rs2) (* (var c) (bv 8 0x20)) false))) (set scaled_part (>> (<< (cast 64 (msb (var part)) (var part)) (var scale) false) (bv 8 0x17) (msb (<< (cast 64 (msb (var part)) (var part)) (var scale) false)))) (set truncated (& (ite (&& (sle (var scaled_part) (bv 64 0x0)) (! (== (var scaled_part) (bv 64 0x0)))) (bv 64 0x0) (ite (! (ule (var scaled_part) (bv 64 0xff))) (bv 64 0xff) (var scaled_part))) (bv 64 0xff))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x8)) false) (* (var c) (bv 8 0x20)) false))) (& (<< (var truncated) (* (var c) (bv 8 0x20)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x8)) false) (* (var c) (bv 8 0x20)) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x18)) false) (+ (* (var c) (bv 8 0x20)) (bv 8 0x8)) false))) (& (<< (& (>> (var rs1) (* (var c) (bv 8 0x20)) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x18)) false)) (+ (* (var c) (bv 8 0x20)) (bv 8 0x8)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x18)) false) (+ (* (var c) (bv 8 0x20)) (bv 8 0x8)) false)))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var res)) (set f32 (cast 64 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x1) false))))
dE "fpackfix f4, f16" a1b007a4 0x0 (seq (set res (bv 32 0x0)) (set c (bv 8 0x0)) (set scale (cast 8 false (cast 5 false (>> (var gsr) (bv 8 0x3) false)))) (set rs2 (fbits (float 1 (append (var f4) (var f5)) ))) (repeat (&& (ule (var c) (bv 8 0x2)) (! (== (var c) (bv 8 0x2)))) (seq (set part (cast 32 (msb (>> (var rs2) (* (var c) (bv 8 0x20)) false)) (>> (var rs2) (* (var c) (bv 8 0x20)) false))) (set scaled_signed_part (>> (<< (cast 64 (msb (var part)) (var part)) (var scale) false) (bv 8 0x10) (msb (<< (cast 64 (msb (var part)) (var part)) (var scale) false)))) (set truncated (cast 32 false (& (ite (&& (sle (var scaled_signed_part) (bv 64 0xffffffffffff8000)) (! (== (var scaled_signed_part) (bv 64 0xffffffffffff8000)))) (bv 64 0xffffffffffff8000) (ite (! (sle (var scaled_signed_part) (bv 64 0x7fff))) (bv 64 0x7fff) (var scaled_signed_part))) (bv 64 0xffff)))) (set res (| (& (var res) (~ (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x10)) false) (* (var c) (bv 8 0x10)) false))) (& (<< (var truncated) (* (var c) (bv 8 0x10)) false) (<< (>> (bv 32 0xffffffff) (- (bv 32 0x20) (bv 32 0x10)) false) (* (var c) (bv 8 0x10)) false)))) (set c (+ (var c) (bv 8 0x1))))) (set bv (var res)) (set f16 (cast 32 false (var bv))) (set fprs (| (var fprs) (<< (bv 3 0x1) (bv 8 0x0) false))))
dE "array8 l0, l2, l4" a9b40212 0x0 (seq (set res (bv 64 0x0)) (set src (var l0)) (set n (cast 8 false (var l2))) (set shft (bv 8 0x0)) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false))) (& (<< (& (>> (var src) (bv 8 0xb) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x0) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false))) (& (<< (& (>> (var src) (bv 8 0x21) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x2) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false))) (& (<< (& (>> (var src) (bv 8 0x37) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false)) (bv 8 0x4) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false))) (& (<< (& (>> (var src) (bv 8 0xd) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false)) (bv 8 0x5) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false))) (& (<< (& (>> (var src) (bv 8 0x23) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0x9) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false))) (& (<< (& (>> (var src) (bv 8 0x38) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0xd) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false))) (& (<< (& (>> (var src) (bv 8 0x3c) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false)))) (branch (is_zero (var n)) empty (seq (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))) (& (<< (& (>> (var src) (bv 8 0x11) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (bv 8 0x11) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))))) (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))) (& (<< (& (>> (var src) (bv 8 0x27) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (+ (bv 8 0x11) (var n)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))))))) (set res (<< (var res) (var shft) false)) (set l4 (var res)))
dE "array16 l0, l2, l4" a9b40252 0x0 (seq (set res (bv 64 0x0)) (set src (var l0)) (set n (cast 8 false (var l2))) (set shft (bv 8 0x1)) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false))) (& (<< (& (>> (var src) (bv 8 0xb) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x0) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false))) (& (<< (& (>> (var src) (bv 8 0x21) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x2) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false))) (& (<< (& (>> (var src) (bv 8 0x37) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false)) (bv 8 0x4) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false))) (& (<< (& (>> (var src) (bv 8 0xd) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false)) (bv 8 0x5) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false))) (& (<< (& (>> (var src) (bv 8 0x23) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0x9) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false))) (& (<< (& (>> (var src) (bv 8 0x38) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0xd) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false))) (& (<< (& (>> (var src) (bv 8 0x3c) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false)))) (branch (is_zero (var n)) empty (seq (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))) (& (<< (& (>> (var src) (bv 8 0x11) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (bv 8 0x11) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))))) (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))) (& (<< (& (>> (var src) (bv 8 0x27) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (+ (bv 8 0x11) (var n)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))))))) (set res (<< (var res) (var shft) false)) (set l4 (var res)))
dE "array32 l0, l2, l4" a9b40292 0x0 (seq (set res (bv 64 0x0)) (set src (var l0)) (set n (cast 8 false (var l2))) (set shft (bv 8 0x2)) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false))) (& (<< (& (>> (var src) (bv 8 0xb) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x0) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x0) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false))) (& (<< (& (>> (var src) (bv 8 0x21) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false)) (bv 8 0x2) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x2)) false) (bv 8 0x2) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false))) (& (<< (& (>> (var src) (bv 8 0x37) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false)) (bv 8 0x4) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x1)) false) (bv 8 0x4) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false))) (& (<< (& (>> (var src) (bv 8 0xd) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false)) (bv 8 0x5) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x3)) false) (bv 8 0x5) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false))) (& (<< (& (>> (var src) (bv 8 0x23) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0x9) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0x9) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false))) (& (<< (& (>> (var src) (bv 8 0x38) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (bv 8 0xd) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (bv 8 0xd) false)))) (set res (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false))) (& (<< (& (>> (var src) (bv 8 0x3c) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false)) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (bv 32 0x4)) false) (+ (bv 8 0x11) (* (bv 8 0x2) (var n))) false)))) (branch (is_zero (var n)) empty (seq (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))) (& (<< (& (>> (var src) (bv 8 0x11) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (bv 8 0x11) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (bv 8 0x11) false))))) (set res (let len (cast 32 false (var n)) (| (& (var res) (~ (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))) (& (<< (& (>> (var src) (bv 8 0x27) false) (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false)) (+ (bv 8 0x11) (var n)) false) (<< (>> (bv 64 0xffffffffffffffff) (- (bv 32 0x40) (var len)) false) (+ (bv 8 0x11) (var n)) false))))))) (set res (<< (var res) (var shft) false)) (set l4 (var res)))
