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