dE "add g1, g2, g3" 86004002 0x0 (set g3 (+ (cast 32 false (var g1)) (cast 32 false (var g2))))
dE "sub g1, g2, g3" 86204002 0x0 (set g3 (- (cast 32 false (var g1)) (cast 32 false (var g2))))
dE "addcc g1, g2, g3" 86804002 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g1)))) (set arg1 (cast 128 false (cast 32 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 32 false (var res128))))
dE "subcc g1, g2, g3" 86a04002 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g1)))) (set arg1 (cast 128 false (cast 32 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 32 false (var res128))))
dE "addx g2, g1, g3" 86408001 0x0 (set g3 (+ (+ (cast 32 false (var g2)) (cast 32 false (var g1))) (ite (lsb (var ccr)) (bv 32 0x1) (bv 32 0x0))))
dE "subx g2, g1, g3" 86608001 0x0 (set g3 (- (- (cast 32 false (var g2)) (cast 32 false (var g1))) (ite (lsb (var ccr)) (bv 32 0x1) (bv 32 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 32 false (var g1)))) (cast 64 false (cast 32 false (var g2)))))) (set g3 (cast 32 false (var res128))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 32 0x7fffffff) (cast 32 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 32 false (var g1)))) (cast 64 (msb (cast 32 false (cast 32 false (var g2)))) (cast 32 false (cast 32 false (var g2)))))) (sdiv (append (cast 32 false (var y)) (cast 32 false (cast 32 false (var g1)))) (cast 64 (msb (cast 32 false (cast 32 false (var g2)))) (cast 32 false (cast 32 false (var g2))))))) (set g3 (cast 32 (msb (var res128)) (var res128))) (set g3 (ite (|| (! (sle (var res128) (bv 128 0x80000000))) (== (var res128) (bv 128 0x80000000))) (bv 32 0x7fffffff) (ite (sle (var res128) (bv 128 0xffffffffffffffffffffffff80000001)) (bv 32 0x80000000) (cast 32 (msb (var res128)) (var res128))))))
dE "umul g1, g2, g3" 86504002 0x0 (seq (set res128 (* (cast 64 false (cast 32 false (cast 32 false (var g1)))) (cast 64 false (cast 32 false (cast 32 false (var g2)))))) (set g3 (cast 32 false (var res128))) (set y (cast 32 false (>> (var res128) (bv 8 0x20) false))))
dE "smul g1, g2, g3" 86584002 0x0 (seq (set res128 (* (cast 64 (msb (cast 32 (msb (cast 32 false (var g1))) (cast 32 false (var g1)))) (cast 32 (msb (cast 32 false (var g1))) (cast 32 false (var g1)))) (cast 64 (msb (cast 32 (msb (cast 32 false (var g2))) (cast 32 false (var g2)))) (cast 32 (msb (cast 32 false (var g2))) (cast 32 false (var g2)))))) (set g3 (cast 32 false (var res128))) (set y (cast 32 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 32 false (var g2))))) (cast 64 false (cast 32 false (cast 32 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 false (cast 32 false (cast 32 false (var g1))))) (cast 64 false (cast 32 false (cast 32 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 32 false (var res128))) (set y (cast 32 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 32 false (var g2))) (cast 32 false (var g2)))) (cast 32 (msb (cast 32 false (var g2))) (cast 32 false (var g2))))) (cast 64 (msb (cast 32 (msb (cast 32 false (var g2))) (cast 32 false (var g2)))) (cast 32 (msb (cast 32 false (var g2))) (cast 32 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 (msb (cast 32 (msb (cast 32 false (var g1))) (cast 32 false (var g1)))) (cast 32 (msb (cast 32 false (var g1))) (cast 32 false (var g1))))) (cast 64 (msb (cast 32 (msb (cast 32 false (var g1))) (cast 32 false (var g1)))) (cast 32 (msb (cast 32 false (var g1))) (cast 32 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 32 false (var res128))) (set y (cast 32 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 32 false (var g2)))))) (set arg1 (cast 128 false (cast 64 false (cast 32 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 32 0x7fffffff) (cast 32 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 32 false (var g2))))) (append (cast 32 false (var y)) (cast 32 false (cast 32 false (var g2)))))) (set arg1 (cast 128 (msb (cast 64 (msb (cast 32 false (cast 32 false (var g1)))) (cast 32 false (cast 32 false (var g1))))) (cast 64 (msb (cast 32 false (cast 32 false (var g1)))) (cast 32 false (cast 32 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 32 0x7fffffff) (ite (sle (var res128) (bv 128 0xffffffffffffffffffffffff80000001)) (bv 32 0x80000000) (cast 32 (msb (var res128)) (var res128))))))
dE "mulscc l1, l2, l3" a7244012 0x0 (seq (set rs1 (cast 32 false (cast 32 false (var l1)))) (set arg0 (cast 128 false (ite (lsb (var y)) (cast 32 false (cast 32 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 32 false (var res128))) (set y (cast 32 false (>> (cast 32 false (var y)) (bv 8 0x1) (lsb (var rs1))))))
dE "and g1, g2, g3" 86084002 0x0 (set g3 (cast 32 false (& (cast 32 false (var g1)) (cast 32 false (var g2)))))
dE "andn g1, g2, g3" 86284002 0x0 (set g3 (cast 32 false (& (cast 32 false (var g1)) (~ (cast 32 false (var g2))))))
dE "or g1, g2, g3" 86104002 0x0 (set g3 (cast 32 false (| (cast 32 false (var g1)) (cast 32 false (var g2)))))
dE "orn g1, g2, g3" 86304002 0x0 (set g3 (cast 32 false (| (cast 32 false (var g1)) (~ (cast 32 false (var g2))))))
dE "xor g1, g2, g3" 86184002 0x0 (set g3 (cast 32 false (^ (cast 32 false (var g1)) (cast 32 false (var g2)))))
dE "xnor g1, g2, g3" 86384002 0x0 (set g3 (cast 32 false (~ (^ (cast 32 false (var g1)) (cast 32 false (var g2))))))
dE "andcc g2, g1, g3" 86888001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (cast 32 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 32 false (var res128))))
dE "andncc g2, g1, g3" 86a88001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (~ (cast 32 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 32 false (var res128))))
dE "orcc g2, g1, g3" 86908001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (cast 32 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 32 false (var res128))))
dE "orncc g2, g1, g3" 86b08001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (~ (cast 32 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 32 false (var res128))))
dE "xorcc g2, g1, g3" 86988001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (cast 32 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 32 false (var res128))))
dE "xnorcc g2, g1, g3" 86b88001 0x0 (seq (set arg0 (cast 128 false (cast 32 false (var g2)))) (set arg1 (cast 128 false (~ (cast 32 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 32 false (var res128))))
dE "jmpl g1+i2, g2" 85c0401a 0x40 (set g2 (bv 32 0x40))
dE "jmpl o1+8, g2" 85c26008 0x40 (set g2 (bv 32 0x40))
dE "jmpl g1, g2" 85c06000 0x40 (set g2 (bv 32 0x40))
dE "call g1+i2" 9fc0401a 0x40 (set o7 (bv 32 0x40))
dE "call o1+8" 9fc26008 0x40 (set o7 (bv 32 0x40))
dE "call g1" 9fc06000 0x40 (set o7 (bv 32 0x40))
dE "ba 0x1000;nop" 1080040001000000 0x0 nop;(branch true (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bn 0x1000;nop" 0080040001000000 0x0 nop;(branch false (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bne 0x1000;nop" 1280040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x2) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "be 0x1000;nop" 0280040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x2) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 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 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bcc 0x1000;nop" 1a80040001000000 0x0 nop;(branch (! (lsb (var ccr))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bcs 0x1000;nop" 0a80040001000000 0x0 nop;(branch (lsb (var ccr)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bpos 0x1000;nop" 1c80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x3) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bneg 0x1000;nop" 0c80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x3) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bvc 0x1000;nop" 1e80040001000000 0x0 nop;(branch (! (lsb (>> (var ccr) (bv 8 0x1) false))) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "bvs 0x1000;nop" 0e80040001000000 0x0 nop;(branch (lsb (>> (var ccr) (bv 8 0x1) false)) (seq (set EA (cast 32 false (cast 32 false (bv 64 0x1000)))) empty (jmp (var EA))) (jmp (bv 32 0x4)))
dE "ldsb [i0+l6], o2" d44e0016 0x0 (set o2 (cast 32 (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 32 (msb (loadw 0 8 (+ (var i0) (bv 32 0x20)))) (loadw 0 8 (+ (var i0) (bv 32 0x20)))))
dE "ldsb [g1], o4" d8484000 0x0 (set o4 (cast 32 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))
dE "ldsh [i0+l6], o2" d4560016 0x0 (set o2 (cast 32 (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 32 (msb (loadw 0 16 (+ (var i0) (bv 32 0x20)))) (loadw 0 16 (+ (var i0) (bv 32 0x20)))))
dE "ldsh [g1], o4" d8504000 0x0 (set o4 (cast 32 (msb (loadw 0 16 (var g1))) (loadw 0 16 (var g1))))
dE "ldub [i0+l6], o2" d40e0016 0x0 (set o2 (cast 32 false (loadw 0 8 (+ (var i0) (var l6)))))
dE "ldub [i0+0x20], o2" d40e2020 0x0 (set o2 (cast 32 false (loadw 0 8 (+ (var i0) (bv 32 0x20)))))
dE "ldub [g1], o2" d4084000 0x0 (set o2 (cast 32 false (loadw 0 8 (var g1))))
dE "lduh [i0+l6], o2" d4160016 0x0 (set o2 (cast 32 false (loadw 0 16 (+ (var i0) (var l6)))))
dE "lduh [i0+0x20], o2" d4162020 0x0 (set o2 (cast 32 false (loadw 0 16 (+ (var i0) (bv 32 0x20)))))
dE "lduh [g1], o2" d4104000 0x0 (set o2 (cast 32 false (loadw 0 16 (var g1))))
dE "ld [i0+l6], o2" d4060016 0x0 (set o2 (cast 32 false (loadw 0 32 (+ (var i0) (var l6)))))
dE "ld [i0+0x20], o2" d4062020 0x0 (set o2 (cast 32 false (loadw 0 32 (+ (var i0) (bv 32 0x20)))))
dE "ld [g1], o2" d4004000 0x0 (set o2 (cast 32 false (loadw 0 32 (var g1))))
dE "ldd [i0+l6], o2" d41e0016 0x0 (seq (set load (loadw 0 64 (+ (var i0) (var l6)))) (set o3 (cast 32 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 32 false (>> (var load) (bv 8 0x20) false))))
dE "ldd [i0+0x20], o2" d41e2020 0x0 (seq (set load (loadw 0 64 (+ (var i0) (bv 32 0x20)))) (set o3 (cast 32 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 32 false (>> (var load) (bv 8 0x20) false))))
dE "ldd [g1], o2" d4184000 0x0 (seq (set load (loadw 0 64 (var g1))) (set o3 (cast 32 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 32 false (>> (var load) (bv 8 0x20) false))))
dE "lda [g1] 1, o2" d4804020 0x0 (set o2 (cast 32 false (loadw 0 32 (var g1))))
dE "ldsba [g1] 1, o2" d4c84020 0x0 (set o2 (cast 32 (msb (loadw 0 8 (var g1))) (loadw 0 8 (var g1))))
dE "lduba [g1] 1, o2" d4884020 0x0 (set o2 (cast 32 false (loadw 0 8 (var g1))))
dE "ldsha [g1] 1, o2" d4d04020 0x0 (set o2 (cast 32 (msb (loadw 0 16 (var g1))) (loadw 0 16 (var g1))))
dE "lduha [g1] 1, o2" d4904020 0x0 (set o2 (cast 32 false (loadw 0 16 (var g1))))
dE "lda [g1] 1, o2" d4804020 0x0 (set o2 (cast 32 false (loadw 0 32 (var g1))))
dE "ldda [g1] 1, o2" d4984020 0x0 (seq (set load (loadw 0 64 (var g1))) (set o3 (cast 32 false (& (var load) (bv 64 0xffffffff)))) (set o2 (cast 32 false (>> (var load) (bv 8 0x20) false))))
dE "ldstuba [i0+l6] 1, o2" d4ee0036 0x0 (seq (set o2 (cast 32 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 32 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 32 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 32 0x20)) (cast 32 false (var o2)))
dE "st o2, [g1]" d4204000 0x0 (storew 0 (var g1) (cast 32 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 32 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 "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 32 false (<< (cast 32 false (cast 32 false (var g1))) (cast 5 false (var g2)) false)))
dE "sll g1, 0x1f, g3" 8728601f 0x0 (set g3 (cast 32 false (<< (cast 32 false (cast 32 false (var g1))) (cast 5 false (bv 64 0x1f)) false)))
dE "srl g1, g2, g3" 87304002 0x0 (set g3 (cast 32 false (>> (cast 32 false (cast 32 false (var g1))) (cast 5 false (var g2)) false)))
dE "srl g1, 0x1f, g3" 8730601f 0x0 (set g3 (cast 32 false (>> (cast 32 false (cast 32 false (var g1))) (cast 5 false (bv 64 0x1f)) false)))
dE "sra g1, g2, g3" 87384002 0x0 (set g3 (cast 32 false (>> (cast 32 false (cast 32 false (var g1))) (cast 5 false (var g2)) (msb (cast 32 false (cast 32 false (var g1)))))))
dE "sra g1, 0x1f, g3" 8738601f 0x0 (set g3 (cast 32 false (>> (cast 32 false (cast 32 false (var g1))) (cast 5 false (bv 64 0x1f)) (msb (cast 32 false (cast 32 false (var g1)))))))
dE "sethi 0x16, g1" 03000016 0x0 (set g1 (cast 32 false (<< (bv 64 0x16) (bv 8 0xa) false)))
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 32 false (var mem_val))))
dE "swap [i0+0x20], o2" d47e2020 0x0 (seq (set mem_val (loadw 0 32 (+ (var i0) (bv 32 0x20)))) (storew 0 (+ (var i0) (bv 32 0x20)) (cast 32 false (var o2))) (set o2 (cast 32 false (var mem_val))))
dE "mov g1, g3" 86100001 0x0 (set g3 (cast 32 false (| (cast 32 false (var g0)) (cast 32 false (var g1)))))
dE "mov 0xff, g3" 861020ff 0x0 (set g3 (cast 32 false (| (cast 32 false (var g0)) (cast 32 false (bv 64 0xff)))))
dE "tle 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 32 false (var o0)) (cast 32 false (var l1)))) (set reg_window_base (* (var cwp) (bv 32 0x200))) (storew 1 (+ (var reg_window_base) (bv 32 0x0)) (var l0)) (storew 1 (+ (var reg_window_base) (bv 32 0x20)) (var l1)) (storew 1 (+ (var reg_window_base) (bv 32 0x40)) (var l2)) (storew 1 (+ (var reg_window_base) (bv 32 0x60)) (var l3)) (storew 1 (+ (var reg_window_base) (bv 32 0x80)) (var l4)) (storew 1 (+ (var reg_window_base) (bv 32 0xa0)) (var l5)) (storew 1 (+ (var reg_window_base) (bv 32 0xc0)) (var l6)) (storew 1 (+ (var reg_window_base) (bv 32 0xe0)) (var l7)) (storew 1 (+ (var reg_window_base) (bv 32 0x100)) (var i0)) (storew 1 (+ (var reg_window_base) (bv 32 0x120)) (var i1)) (storew 1 (+ (var reg_window_base) (bv 32 0x140)) (var i2)) (storew 1 (+ (var reg_window_base) (bv 32 0x160)) (var i3)) (storew 1 (+ (var reg_window_base) (bv 32 0x180)) (var i4)) (storew 1 (+ (var reg_window_base) (bv 32 0x1a0)) (var i5)) (storew 1 (+ (var reg_window_base) (bv 32 0x1c0)) (var fp)) (storew 1 (+ (var reg_window_base) (bv 32 0x1e0)) (var i7)) (set cwp (mod (- (var cwp) (bv 32 0x1)) (bv 32 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 32 0x0)) (set l1 (bv 32 0x0)) (set l2 (bv 32 0x0)) (set l3 (bv 32 0x0)) (set l4 (bv 32 0x0)) (set l5 (bv 32 0x0)) (set l6 (bv 32 0x0)) (set l7 (bv 32 0x0)) (set o0 (bv 32 0x0)) (set o1 (bv 32 0x0)) (set o2 (bv 32 0x0)) (set o3 (bv 32 0x0)) (set o4 (bv 32 0x0)) (set o5 (bv 32 0x0)) (set sp (bv 32 0x0)) (set o7 (bv 32 0x0)) (set i7 (var add_result)))
dE "restore o0, l1, i7" bfea0011 0x0 (seq (set add_result (+ (cast 32 false (var o0)) (cast 32 false (var l1)))) (set cwp (mod (+ (var cwp) (bv 32 0x1)) (bv 32 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 32 0x200))) (set l0 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x0)))) (set l1 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x20)))) (set l2 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x40)))) (set l3 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x60)))) (set l4 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x80)))) (set l5 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xa0)))) (set l6 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xc0)))) (set l7 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xe0)))) (set i0 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x100)))) (set i1 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x120)))) (set i2 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x140)))) (set i3 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x160)))) (set i4 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x180)))) (set i5 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1a0)))) (set fp (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1c0)))) (set i7 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1e0)))) (set i7 (var add_result)))
dE "rett i7+8" 81cfe008 0x0 (seq (set tnpc (cast 32 false (+ (var i7) (bv 32 0x8)))) empty (set cwp (mod (+ (var cwp) (bv 32 0x1)) (bv 32 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 32 0x200))) (set l0 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x0)))) (set l1 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x20)))) (set l2 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x40)))) (set l3 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x60)))) (set l4 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x80)))) (set l5 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xa0)))) (set l6 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xc0)))) (set l7 (loadw 1 32 (+ (var reg_window_base) (bv 32 0xe0)))) (set i0 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x100)))) (set i1 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x120)))) (set i2 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x140)))) (set i3 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x160)))) (set i4 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x180)))) (set i5 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1a0)))) (set fp (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1c0)))) (set i7 (loadw 1 32 (+ (var reg_window_base) (bv 32 0x1e0)))) empty)
