(declare-fun a () (Array (_ BitVec 4) Float16))
(assert (= (select a (_ bv0 4)) (fp (_ bv1 1) (_ bv0 5) (_ bv0 10))))
(assert (= a (store a (_ bv0 4) (fp (_ bv0 1) (_ bv0 5) (_ bv0 10)))))
(set-info :status unsat)
(check-sat)