sat
(model
	(define-fun cat () (_ BitVec 16) (_ bv7 16)) ; 0x7
	(define-fun dog () (_ BitVec 16) (_ bv17 16)) ; 0x11
	(define-fun rabbit () (_ BitVec 16) (_ bv3 16)) ; 0x3
)