(declare-fun fun (
  (_ BitVec 32))		; no supported for UF yet