(bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t))