sat
(model
    (define-fun m () (_ BitVec 16) (_ bv10923 16)) ; 0x2aab
    (define-fun a () (_ BitVec 16) (_ bv1554 16)) ; 0x612
    (define-fun b () (_ BitVec 16) (_ bv1554 16)) ; 0x612
)