(declare-fun f () (_ BitVec 1))
(assert (let ((f (_ bv1 1)))