d "mrs r0, primask" eff31080
d "msr basepri, r3" 83f31188
d "vcgt.f16 d17, d1, d4" 71ff041e 0 (seq empty (set d17 (<< (cast 64 false (ite (! (sle (cast 16 false (>> (var d1) (bv 8 0x0) false)) (cast 16 false (>> (var d4) (bv 8 0x0) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x0) false)) (set d17 (<< (cast 64 false (ite (! (sle (cast 16 false (>> (var d1) (bv 8 0x10) false)) (cast 16 false (>> (var d4) (bv 8 0x10) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x10) false)) (set d17 (<< (cast 64 false (ite (! (sle (cast 16 false (>> (var d1) (bv 8 0x20) false)) (cast 16 false (>> (var d4) (bv 8 0x20) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x20) false)) (set d17 (<< (cast 64 false (ite (! (sle (cast 16 false (>> (var d1) (bv 8 0x30) false)) (cast 16 false (>> (var d4) (bv 8 0x30) false)))) (~ (bv 16 0x0)) (bv 16 0x0))) (bv 8 0x30) false)))
