% z3 -smt2 3.smt > 3.txt

sat
(model 
  (define-fun x () (_ BitVec 16)
    #x000e)
)