d "sats.l d0" 4c80 0x0 (seq (set src (var d0)) (set res (ite (! (is_zero (& (cast 8 false (var sr)) (bv 8 0x2)))) (ite (msb (var src)) (bv 32 0x7fffffff) (bv 32 0x80000000)) (var src))) (set d0 (cast 32 false (var res))) (set sr (| (& (var sr) (bv 16 0xff00)) (cast 16 false (cast 8 false (| (| (& (| (& (| (& (| (& (& (cast 8 false (var sr)) (bv 8 0xe0)) (bv 8 0xf7)) (<< (ite (msb (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x3) false)) (bv 8 0xfb)) (<< (ite (is_zero (cast 32 false (var res))) (bv 8 0x1) (bv 8 0x0)) (bv 8 0x2) false)) (bv 8 0xfd)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x1) false)) (bv 8 0xfe)) (<< (ite false (bv 8 0x1) (bv 8 0x0)) (bv 8 0x0) false)) (& (cast 8 false (var sr)) (bv 8 0x10))))))))
