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