(assert
(bvnot bvnot)