Advertisement
Guest User

Untitled

a guest
Sep 30th, 2016
49
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.03 KB | None | 0 0
  1. (declare-fun a () (_ BitVec 64))
  2. (declare-fun b () (_ BitVec 64))
  3. (declare-fun c () (_ BitVec 64))
  4. (declare-fun d () (_ BitVec 64))
  5. (declare-fun e () (_ BitVec 64))
  6. (declare-fun f () (_ BitVec 64))
  7. (declare-fun g () (_ BitVec 64))
  8. (declare-fun h () (_ BitVec 64))
  9. (declare-fun i () (_ BitVec 64))
  10. (declare-fun j () (_ BitVec 64))
  11. (declare-fun k () (_ BitVec 64))
  12. (declare-fun l () (_ BitVec 64))
  13. (declare-fun m () (_ BitVec 64))
  14. (declare-fun n () (_ BitVec 64))
  15. (declare-fun o () (_ BitVec 64))
  16. (declare-fun p () (_ BitVec 64))
  17. (declare-fun q () (_ BitVec 64))
  18. (declare-fun r () (_ BitVec 64))
  19. (declare-fun s () (_ BitVec 64))
  20. (declare-fun t () (_ BitVec 64))
  21. (declare-fun u () (_ BitVec 64))
  22. (declare-fun v () (_ BitVec 64))
  23. (declare-fun w () (_ BitVec 64))
  24. (declare-fun x () (_ BitVec 64))
  25. (declare-fun y () (_ BitVec 64))
  26. (declare-fun z () (_ BitVec 64))
  27.  
  28. (assert (= #x00000000
  29. (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)))
  30. (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))
  31.  
  32. (check-sat)
  33. (get-model)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement