% z3 -smt2 2.smt

sat
(model 
  (define-fun z () (_ BitVec 16)
    #x0005)
  (define-fun y () (_ BitVec 16)
    #x0003)
  (define-fun x () (_ BitVec 16)
    #x0002)
)