Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (declare-fun a () (_ BitVec 64))
- (declare-fun b () (_ BitVec 64))
- (declare-fun c () (_ BitVec 64))
- (declare-fun d () (_ BitVec 64))
- (declare-fun e () (_ BitVec 64))
- (declare-fun f () (_ BitVec 64))
- (declare-fun g () (_ BitVec 64))
- (declare-fun h () (_ BitVec 64))
- (declare-fun i () (_ BitVec 64))
- (declare-fun j () (_ BitVec 64))
- (declare-fun k () (_ BitVec 64))
- (declare-fun l () (_ BitVec 64))
- (declare-fun m () (_ BitVec 64))
- (declare-fun n () (_ BitVec 64))
- (declare-fun o () (_ BitVec 64))
- (declare-fun p () (_ BitVec 64))
- (declare-fun q () (_ BitVec 64))
- (declare-fun r () (_ BitVec 64))
- (declare-fun s () (_ BitVec 64))
- (declare-fun t () (_ BitVec 64))
- (declare-fun u () (_ BitVec 64))
- (declare-fun v () (_ BitVec 64))
- (declare-fun w () (_ BitVec 64))
- (declare-fun x () (_ BitVec 64))
- (declare-fun y () (_ BitVec 64))
- (declare-fun z () (_ BitVec 64))
- (assert (= #x00000000
- (bvxor a b c d e f g h i j k l m n o p q r s t u v w x y z)))
- (assert (distinct a b c d e f g h i j k l m n o p q r s t u v w x y z))
- (check-sat)
- (get-model)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement