sat
(model
	(define-fun a () (_ BitVec 64) (_ bv1679813589618343937 64)) ; 0x174fe58f4a134001
	(define-fun b () (_ BitVec 64) (_ bv1648532086516097041 64)) ; 0x16e0c332c9a02011
	(define-fun c () (_ BitVec 64) (_ bv431124923357184020 64)) ; 0x5fba9d56685c014
	(define-fun d () (_ BitVec 64) (_ bv1700335937406039020 64)) ; 0x1798ce86bbeaf3ec
)