sat
(
  (define-fun v0 () (_ BitVec 4) #b0001)
)