(assert (bvand (_ bv0 1)(_ bv0 2))