(declare-const v (_ BitVec 5))
(assert (= true (fp #b01 #x73e749afad3c7 v)))